mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.dual_map : ∀ {X Y : NonemptyFinLinOrd} (f : X ⟶ Y),
  NonemptyFinLinOrd.dual.map f = NonemptyFinLinOrd.ofHom (OrderHom.dual (LinOrd.Hom.hom f.hom))
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsLimitsOfShapeFintypeCatDiscretePEmpty : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.Limits.ReflectsLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F
-- Mathlib.LinearAlgebra.Multilinear.Pi
MultilinearMap.piFamilyₗ_apply : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : CommSemiring R] [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)]
  [inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)] [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)]
  [inst_4 : (p : (i : ι) → κ i) → Module R (N p)]
  (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)),
  MultilinearMap.piFamilyₗ f = MultilinearMap.piFamily f
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenCoend.map_comp_assoc : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C]
  {G H : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (f : F ⟶ G) (g : G ⟶ H) {Z : C}
  (h : CategoryTheory.Limits.chosenCoend H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.map g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.map (CategoryTheory.CategoryStruct.comp f g))
      h
-- Mathlib.Data.Sym.Sym2
/-- **Alias** of `Sym2.diagSet_eq_setOfPred_isDiag`. -/
Sym2.diagSet_eq_setOf_isDiag : ∀ {α : Type u_1}, Sym2.diagSet = {z | z.IsDiag}
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.moment_zero : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {p : ℕ} {μ : MeasureTheory.Measure Ω},
  p ≠ 0 → ProbabilityTheory.moment 0 p μ = 0
-- Lean.Server.InfoUtils
/-- Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves).  -/
Lean.Elab.InfoTree.collectNodesBottomUp : {α : Type} →
  (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List α → List α) →
    Lean.Elab.InfoTree → List α
-- Lean.Elab.Syntax
/-- Given a `stx` of category `syntax`, return a `(newStx, lhsPrec?)`,
where `newStx` is of category `term`. After elaboration, `newStx` should have type
`TrailingParserDescr` if `lhsPrec?.isSome`, and `ParserDescr` otherwise.  -/
Lean.Elab.Term.toParserDescr : Lean.Syntax → Lean.Name → Lean.Elab.TermElabM (Lean.Term × Option ℕ)
-- Mathlib.Data.Nat.MaxPowDiv
Nat.divMaxPow_self : ∀ {p : ℕ}, p ≠ 0 → p.divMaxPow p = 1
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.StrongTrans F G) {a b : B} {a' : C} {f g : a ⟶ b}
  (β : f ⟶ g) (h : G.obj b ⟶ a') {Z : F.obj a ⟶ a'}
  (h_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (η.app a) (G.map g)) h ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.map₂ β) (η.app b)) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality g).hom h) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) h).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) h))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map g) h).inv h_1)))
-- Mathlib.GroupTheory.Sylow
Sylow.smul_eq_of_normal : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {g : G} {P : Sylow p G} [h : (↑P).Normal], g • P = P
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.openCell_subset_skeletonLT : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n),
  Topology.RelCWComplex.openCell n j ⊆ ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1))
-- Mathlib.LinearAlgebra.PiTensorProduct.Finsupp
PiTensorProduct.ofFinsuppEquiv_tprod_single : ∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [inst : CommSemiring R] [inst_1 : Fintype ι]
  [inst_2 : DecidableEq ι] [inst_3 : (i : ι) → DecidableEq (κ i)] [inst_4 : (i : ι) → AddCommMonoid (M i)]
  [inst_5 : (i : ι) → Module R (M i)] [inst_6 : (i : ι) → DecidableEq (M i)] (p : (i : ι) → κ i) (m : (i : ι) → M i),
  PiTensorProduct.ofFinsuppEquiv ((PiTensorProduct.tprod R) fun i => fun₀ | p i => m i) = fun₀ | p => ⨂ₜ[R] (i : ι), m i
-- Lean.Data.Json.Basic
Lean.Json.bool.inj : ∀ {b b_1 : Bool}, Lean.Json.bool b = Lean.Json.bool b_1 → b = b_1
-- Mathlib.Topology.UniformSpace.Completion
/-- The uniform isomorphism between two completions of isomorphic uniform spaces.  -/
UniformSpace.Completion.mapEquiv : {α : Type u_1} →
  [inst : UniformSpace α] →
    {β : Type u_2} → [inst_1 : UniformSpace β] → α ≃ᵤ β → UniformSpace.Completion α ≃ᵤ UniformSpace.Completion β
-- Mathlib.FieldTheory.Relrank
Subfield.inf_relrank_right : ∀ {E : Type v} [inst : Field E] (A B : Subfield E), (A ⊓ B).relrank B = A.relrank B
-- Mathlib.Tactic.ClickSuggestions.Unfold
/-- Append the unfoldings of `e` to `acc`. Assume `e` is in `whnfCore` form.  -/
_private.Mathlib.Tactic.ClickSuggestions.Unfold.0.Mathlib.Tactic.ClickSuggestions.unfolds.go : Lean.Expr → Array Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered : ∀ {S : AlgebraicGeometry.Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) [AlgebraicGeometry.QuasiCompactCover 𝒰]
  {U : S.Opens}, AlgebraicGeometry.IsAffineOpen U → IsCompactOpenCovered (fun x => ⇑(𝒰.f x)) ↑U
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.of_bijective : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsAdicComplete I M], Function.Bijective ⇑(AdicCompletion.of I M)
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal},
  AEMeasurable f μ →
    (∀ᵐ (x : α) ∂μ, f x < ⊤) → ∀ (g : α → ENNReal), ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
-- Mathlib.CategoryTheory.Action.Basic
Action.resCongr_inv : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [inst_1 : Monoid G]
  [inst_2 : Monoid H] {f f' : G →* H} (h : f = f'),
  (Action.resCongr V h).inv = { app := fun X => (Action.mkIso (CategoryTheory.Iso.refl X.V) ⋯).inv, naturality := ⋯ }
-- Mathlib.Data.Int.Bitwise
Int.bitwise_bit : ∀ (f : Bool → Bool → Bool) (a : Bool) (m : ℤ) (b : Bool) (n : ℤ),
  Int.bitwise f (Int.bit a m) (Int.bit b n) = Int.bit (f a b) (Int.bitwise f m n)
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.CompleteEquipartiteSubgraph.mk : {V : Type u_1} →
  {G : SimpleGraph V} →
    {r t : ℕ} →
      (parts : Finset (Finset V)) →
        parts.card = r ∨ t = 0 →
          (∀ {p : Finset V}, p ∈ parts → p.card = t) →
            ((↑parts).Pairwise fun x1 x2 => G.IsCompleteBetween ↑x1 ↑x2) → G.CompleteEquipartiteSubgraph r t
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasMultiequalizer I] {W : C}
  (i j : W ⟶ CategoryTheory.Limits.multiequalizer I),
  (∀ (a : J.L),
      CategoryTheory.CategoryStruct.comp i (CategoryTheory.Limits.Multiequalizer.ι I a) =
        CategoryTheory.CategoryStruct.comp j (CategoryTheory.Limits.Multiequalizer.ι I a)) →
    i = j
-- Init.Data.String.Lemmas.FindPos
String.posGE_le_iff : ∀ {s : String} {p : String.Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos}, s.posGE p h ≤ q ↔ p ≤ q.offset
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_c : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : AlgebraicGeometry.PresheafedSpace C}
  (Y : AlgebraicGeometry.SheafedSpace C) (f : X ⟶ Y.toPresheafedSpace)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom Y f).hom.c = f.c
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.MIntl.mk.sizeOf_spec : ∀ {F : PFunctor.{uA, uB}} (approx : (n : ℕ) → PFunctor.Approx.CofixA F n)
  (consistent : PFunctor.Approx.AllAgree approx), sizeOf { approx := approx, consistent := consistent } = 1
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus_self_sub_right : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : AddGroup N] (f g : α →₀ N),
  f.neLocus (f - g) = g.support
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- An equivalence of categories lifts to an equivalence of their commutative monoid objects.  -/
CategoryTheory.Equivalence.mapCommMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                (e : C ≌ D) →
                  [inst_6 : e.functor.Braided] →
                    [inst_7 : e.inverse.Braided] → [e.IsMonoidal] → CategoryTheory.CommMon C ≌ CategoryTheory.CommMon D
-- Mathlib.Data.Nat.Log
Nat.clog.go.eq_def : ∀ (n a a_1 : ℕ),
  Nat.clog.go n a a_1 =
    match a, a_1 with
    | b, 0 => (b / n, 0)
    | b, fuel.succ =>
      if n ≤ b then (b / n, 0)
      else
        match Nat.clog.go n (b * b) fuel with
        | (q, e) => if q < b then (q, 2 * e + 1) else (q / b, 2 * e)
-- Init.Data.Float.Model.Float
/-- The underlying bit pattern is valid according to the IEEE `binary64` format.  -/
Float.Model.valid : ∀ (self : Float.Model), Float.Model.Format.binary64.Valid self.toBits.toBitVec
-- Mathlib.RingTheory.Int.Basic
Int.Prime.dvd_mul : ∀ {m n : ℤ} {p : ℕ}, Nat.Prime p → ↑p ∣ m * n → p ∣ m.natAbs ∨ p ∣ n.natAbs
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.bernoulliMeasure_def : ∀ {X : Type u_1} [inst : MeasurableSpace X] (x y : X) (p : ↑unitInterval),
  ProbabilityTheory.bernoulliMeasure x y p =
    unitInterval.toNNReal p • MeasureTheory.Measure.dirac x +
      unitInterval.toNNReal (unitInterval.symm p) • MeasureTheory.Measure.dirac y
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.mul : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop} (j : J)
  (x y : ↑(F.obj j)), RingCat.Colimits.Relation.below ⋯
-- Init.Data.Vector.Attach
Vector.pmap_push : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {P : α → Prop} {f : (a : α) → P a → β} {a : α} {xs : Vector α n}
  {h : ∀ b ∈ xs.push a, P b}, Vector.pmap f (xs.push a) h = (Vector.pmap f xs ⋯).push (f a ⋯)
-- Mathlib.Data.Seq.Defs
/-- Convert a sequence into either a list or a stream depending on whether
it is finite or infinite. (Without decidability of the infiniteness predicate,
this is not constructively possible.)  -/
Stream'.Seq.toListOrStream : {α : Type u} → (s : Stream'.Seq α) → [Decidable s.Terminates] → List α ⊕ Stream' α
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup_of_inclusion.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α} (hst : t ⊆ s),
  SubAddAction.ofFixingAddSubgroup_of_inclusion M hst = { toFun := fun y => ⟨↑y, ⋯⟩, map_vadd' := ⋯ }
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.hom_id : ∀ {A : ProfiniteAddGrp.{u}},
  ProfiniteAddGrp.Hom.hom (CategoryTheory.CategoryStruct.id A) = ContinuousAddMonoidHom.id ↑A.toProfinite.toTop
-- Mathlib.LinearAlgebra.Ray
sameRay_neg_smul_right_iff_of_ne : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [Module.IsTorsionFree R M] {v : M} {r : R},
  v ≠ 0 → r ≠ 0 → (SameRay R (-v) (r • v) ↔ r < 0)
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsClosedImmersion.iff_isFinite_and_mono : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.IsClosedImmersion f ↔ AlgebraicGeometry.IsFinite f ∧ CategoryTheory.Mono f
-- Lean.Elab.PreDefinition.Structural.BRecOn
/-- Given the `motives`, pass the right universe levels, the parameters, and the motives.
It was already checked earlier in `checkCodomainsLevel` that the functions live in the same universe.
 -/
Lean.Elab.Structural.mkBRecOnConst : Array Lean.Elab.Structural.RecArgInfo →
  Lean.Elab.Structural.Positions → Array Lean.Expr → Bool → Lean.MetaM (ℕ → Lean.Expr)
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instCommGroup : {α : Type u_1} → [CommGroup α] → CommGroup αᵐᵒᵖ
-- Mathlib.LinearAlgebra.FiniteSpan
/-- A linear equivalence which preserves a finite spanning set must have finite order.  -/
LinearEquiv.isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {Φ : Set M},
  Φ.Finite → Submodule.span R Φ = ⊤ → ∀ {e : M ≃ₗ[R] M}, Set.MapsTo (⇑e) Φ Φ → IsOfFinOrder e
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.ne_top_iff_exists_not_adj : ∀ {V : Type u} {G : SimpleGraph V}, G ≠ ⊤ ↔ ∃ a b, a ≠ b ∧ ¬G.Adj a b
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_le_re : ∀ {K : Type u_1} [inst : RCLike K] {x y : K}, x ≤ y → RCLike.re x ≤ RCLike.re y
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.sub_right : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G} (c : G), a ≡ b [PMOD p] → a - c ≡ b - c [PMOD p]
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.ιR_jointly_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) (r : ↑cR.pt),
  ∃ U a, (PresheafOfModules.ModuleColimit.ιR cR) a = r
-- Lean.Elab.Syntax
/-- (Try to) add a term info for the alias with info `info` at `ref`.  -/
Lean.Elab.Term.addAliasInfo : Lean.Syntax → Lean.Parser.ParserAliasInfo → Lean.Elab.TermElabM Unit
-- Mathlib.Order.SuccPred.Basic
Order.succ_ne_bot : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : OrderBot α] [Nontrivial α] (a : α),
  Order.succ a ≠ ⊥
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.linearIsometryBoundedOfCompact_symm_apply : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] {𝕜 : Type u_4} [inst_3 : NormedRing 𝕜] [inst_4 : Module 𝕜 E]
  [inst_5 : IsBoundedSMul 𝕜 E] (f : BoundedContinuousFunction α E),
  (ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).symm f = f.toContinuousMap
-- Mathlib.Util.CountHeartbeats
/-- `#count_heartbeats! in cmd` runs a command `10` times, reporting the range in heartbeats, and the
standard deviation. The command `#count_heartbeats! n in cmd` runs it `n` times instead.

Example usage:
```
#count_heartbeats! in
def f := 37
```
displays the info message `Min: 7 Max: 8 StdDev: 14%`.
 -/
Mathlib.CountHeartbeats.«command#count_heartbeats!_In__» : Lean.ParserDescr
-- Lean.Elab.Arg
Lean.Elab.Term.NamedArg.ref : Lean.Elab.Term.NamedArg → Lean.Syntax
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftShift_units_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n : ℤ}
  (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n') (x : Rˣ),
  (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn'
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.toList_toArray : ∀ {α : Type u} {r : Std.Roi α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α], r.toArray.toList = r.toList
-- Mathlib.Analysis.Convex.Basic
Antitone.convex_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {f : E → β}, Antitone f → ∀ (r : β), Convex 𝕜 {x | f x < r}
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.any.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → (α → Bool) → Sort u_2) (h : α) (t : List α) (p : α → Bool)
  (h_1 : (x : α → Bool) → motive [] x) (h_2 : (h : α) → (t : List α) → (p : α → Bool) → motive (h :: t) p),
  (match h :: t, p with
    | [], x => h_1 x
    | h :: t, p => h_2 h t p) =
    h_2 h t p
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
/-- Any power of function from a well-formed basis' tail is Majorized by
basis' head with zero exponent.  -/
Tactic.ComputeAsymptotics.WellFormedBasis.tail_pow_majorized_head : ∀ {hd f : ℝ → ℝ} {tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis (hd :: tl) →
    f ∈ tl → ∀ (r : ℝ), Tactic.ComputeAsymptotics.Majorized (f ^ r) hd 0
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.instNeg : (R : Type u) → (X : Type v) → [inst : CommRing R] → Neg (FreeLieAlgebra R X)
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.maxEntry?.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) (size : ℕ) (k : α)
  (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β) →
                  (l_2 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1))),
  (match Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1) =>
      h_3 size k v l r size_2 k_2 v_2 l_2 r_1 h) =
    h_3 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯
-- Mathlib.Algebra.Order.GroupWithZero.Lex
MonoidWithZeroHom.snd_mono : ∀ {M₀ : Type u_1} {N₀ : Type u_2} [inst : GroupWithZero M₀] [inst_1 : Preorder M₀]
  [inst_2 : LinearOrderedCommGroupWithZero N₀], Monotone ⇑(MonoidWithZeroHom.snd M₀ N₀)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.baseChange_dblY : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Jacobian R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P : Fin 3 → A), (W'.baseChange B).dblY (⇑f ∘ P) = f ((W'.baseChange A).dblY P)
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.coe_sInf' : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α} (S : Set ↥L), ↑(sInf S) = ⨅ N ∈ S, ↑N
-- Std.Sync.Broadcast
/-- Maps receiver IDs to their current position in the message sequence.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.State.receivers : {α : Type} → Std.Bounded.State✝ α → Std.TreeMap ℕ ℕ compare
-- Mathlib.Topology.Compactness.Lindelof
/-- A closed embedding is proper, i.e., inverse images of Lindelöf sets are contained in Lindelöf.
Moreover, the preimage of a Lindelöf set is Lindelöf, see
`Topology.IsClosedEmbedding.isLindelof_preimage`.  -/
Topology.IsClosedEmbedding.tendsto_coLindelof : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsClosedEmbedding f → Filter.Tendsto f (Filter.coLindelof X) (Filter.coLindelof Y)
-- Init.Data.Stream
Std.Stream.mk : {stream : Type u} → {value : outParam (Type v)} → (stream → Option (value × stream)) → Std.Stream stream value
-- Init.Data.Slice.List.Lemmas
List.toList_mkSlice_rii_eq_toList_mkSlice_rco : ∀ {α : Type u_1} {xs : List α},
  Std.Slice.toList (Std.Rii.Sliceable.mkSlice xs *...*) = Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs 0...xs.length)
-- Mathlib.Algebra.BigOperators.Finsupp.Fin
finTwoArrowEquiv'_symm_apply : ∀ (M : Type u_1) [inst : Zero M] (a : M × M), (finTwoArrowEquiv' M).symm a = Finsupp.equivFunOnFinite.symm ![a.1, a.2]
-- Mathlib.RingTheory.Coalgebra.Basic
Prod.instCoalgebra : (R : Type u) →
  (A : Type v) →
    (B : Type w) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : AddCommMonoid B] →
            [inst_3 : Module R A] → [inst_4 : Module R B] → [Coalgebra R A] → [Coalgebra R B] → Coalgebra R (A × B)
-- Mathlib.Algebra.Ring.GeomSum
geom_sum_mul : ∀ {R : Type u_1} [inst : Ring R] (x : R) (n : ℕ), (∑ i ∈ Finset.range n, x ^ i) * (x - 1) = x ^ n - 1
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.hom_inv_id_hom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A} (e : F ≅ G) (n : A),
  CategoryTheory.CategoryStruct.comp (e.hom.hom n) (e.inv.hom n) = CategoryTheory.CategoryStruct.id (F.functor n)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_emptyWithCapacity : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {a : α} {c : ℕ},
  Std.DHashMap.Const.get? (Std.DHashMap.emptyWithCapacity c) a = none
-- Mathlib.Algebra.Homology.HomotopyCategory
homotopy_congruence : ∀ {ι : Type u_2} (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (c : ComplexShape ι), CategoryTheory.Congruence (homotopic V c)