mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentSymbolAux : {Self : Type} → [Lean.ToJson Self] → Lean.ToJson (Lean.Lsp.DocumentSymbolAux Self)
-- Lean.Parser.Types
Lean.Parser.ParserCacheKey.toCacheableParserContext : Lean.Parser.ParserCacheKey → Lean.Parser.CacheableParserContext
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- The `f` and `h` in the Weierstrass preparation theorem are unique.

This result is stated using two `PowerSeries.IsWeierstrassFactorization` assertions, and only
requires the ring being Hausdorff with respect to the maximal ideal. If you want `f` and `h` equal
to `PowerSeries.weierstrassDistinguished` and `PowerSeries.weierstrassUnit`,
use `PowerSeries.IsWeierstrassFactorization.unique` instead, which requires the ring being
complete with respect to the maximal ideal.  -/
PowerSeries.IsWeierstrassFactorization.elim : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] [IsHausdorff (IsLocalRing.maximalIdeal A) A]
  {g : PowerSeries A} {f f' : Polynomial A} {h h' : PowerSeries A},
  g.IsWeierstrassFactorization f h → g.IsWeierstrassFactorization f' h' → f = f' ∧ h = h'
-- Mathlib.Algebra.Group.Center
Set.addCentralizer_eq_univ : ∀ (M : Type u_1) {S : Set M} [inst : AddCommSemigroup M], S.addCentralizer = Set.univ
-- Aesop.Forward.RuleInfo
/-- Slots representing the maximal premises of the forward rule, partitioned
into metavariable clusters.  -/
Aesop.ForwardRuleInfo.slotClusters : Aesop.ForwardRuleInfo → Array (Array Aesop.Slot)
-- Mathlib.SetTheory.Cardinal.ENat
/-- **Alias** of `Cardinal.toENat_le_natCast`. -/
Cardinal.toENat_le_nat : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.toENat c ≤ ↑n ↔ c ≤ ↑n
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.hom_ofHom : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : CommRing X] [inst_2 : Bialgebra R X] [inst_3 : CommRing Y]
  [inst_4 : Bialgebra R Y] (f : X →ₐc[R] Y), CommBialgCat.Hom.hom (CommBialgCat.ofHom f) = f
-- Mathlib.Data.List.Defs
List.iterateTR.loop.eq_1 : ∀ {α : Type u_1} (f : α → α) (a : α) (l : List α), List.iterateTR.loop f a 0 l = l.reverse
-- Mathlib.Algebra.Star.UnitaryStarAlgAut
Unitary.conjStarAlgAut_symm : ∀ {S : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : SMul S R]
  [inst_3 : IsScalarTower S R R] [inst_4 : SMulCommClass S R R] (u : ↥(unitary R)),
  ((Unitary.conjStarAlgAut S R) u).symm = (Unitary.conjStarAlgAut S R) (star u)
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Insert an element into the set, preserving balance and the BST property.
If an equivalent element is already in the set, this replaces it.

```
insert 1 {1, 2, 3} = {1, 2, 3}
insert 4 {1, 2, 3} = {1, 2, 3, 4}
```

Using a preorder on `ℕ × ℕ` that only compares the first coordinate:

```
insert (1, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 1)}
insert (3, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2), (3, 1)}
```  -/
Ordnode.insert : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → Ordnode α
-- Mathlib.Condensed.Light.Small
LightCondensed.instSmallHom : ∀ {C : Type w} [inst : CategoryTheory.Category.{v, w} C] (X Y : LightCondensed C),
  Small.{max u v, max (u + 1) v} (X ⟶ Y)
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {F : ι → Type u_4} {G : ι → Type u_5} {H : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (F i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_3 : (i : ι) → NormedAddCommGroup (G i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (G i)] [inst_5 : NormedAddCommGroup H]
  [inst_6 : NormedSpace 𝕜 H] [inst_7 : Fintype ι] [inst_8 : DecidableEq ι]
  (fg : ContinuousMultilinearMap 𝕜 G H × ((i : ι) → F i →L[𝕜] G i)),
  HasStrictFDerivAt (fun fg => fg.1.compContinuousLinearMap fg.2)
    (ContinuousMultilinearMap.compContinuousLinearMapL fg.2 ∘SL
        ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i) +
      fg.1.fderivCompContinuousLinearMap fg.2 ∘SL
        ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i))
    fg
-- Mathlib.Data.Fintype.Sets
/-- **Alias** of `Set.toFinset_ofPred`. -/
Set.toFinset_setOf : ∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : Fintype ↑{x | p x}],
  {x | p x}.toFinset = Finset.filter p Finset.univ
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.preservesZeroMorphisms_of_full : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [F.Full], F.PreservesZeroMorphisms
-- Mathlib.Data.List.Lex
List.Lex.imp : ∀ {α : Type u} {r s : α → α → Prop},
  (∀ (a b : α), r a b → s a b) → ∀ (l₁ l₂ : List α), List.Lex r l₁ l₂ → List.Lex s l₁ l₂
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
instGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  (G : Type u) →
                                    [inst_9 : TopologicalSpace G] →
                                      [inst_10 : ChartedSpace H G] →
                                        [inst_11 : Group G] →
                                          [LieGroup I (↑⊤) G] →
                                            (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) →
                                              Group ((smoothSheaf IM I M G).presheaf.obj U)
-- Mathlib.GroupTheory.Torsion
/-- The free rank of a finitely generated abelian group is the rank of its free part.  -/
AddCommGroup.freeRank : (G : Type u_1) → [inst : AddCommGroup G] → [AddGroup.FG G] → ℕ
-- Init.Data.Int.DivMod.Lemmas
Int.add_fmod_right : ∀ (a b : ℤ), (a + b).fmod b = a.fmod b
-- Mathlib.Combinatorics.Additive.RuzsaCovering
/-- **Ruzsa's covering lemma**.  -/
Finset.ruzsa_covering_mul : ∀ {G : Type u_1} [inst : Group G] {K : ℝ} [inst_1 : DecidableEq G] {A B : Finset G},
  B.Nonempty → ↑(A * B).card ≤ K * ↑B.card → ∃ F ⊆ A, ↑F.card ≤ K ∧ A ⊆ F * (B / B)
-- Lean.Parser.Term.Doc
/-- The recommended spelling of the notation in identifiers.  -/
Lean.Parser.Term.Doc.RecommendedSpelling.recommendedSpelling : Lean.Parser.Term.Doc.RecommendedSpelling → String
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instSMul : {α : Type u_1} →
  {R : Type u_3} → [inst : SMul R ENNReal] → [IsScalarTower R ENNReal ENNReal] → SMul R (MeasureTheory.OuterMeasure α)
-- Mathlib.Analysis.Normed.Order.UpperLower
IsClopen.lowerClosure_pi : ∀ {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)}, IsClopen s → BddAbove s → IsClopen ↑(lowerClosure s)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inv_eq_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] {s : Finset α}, s⁻¹ = ∅ ↔ s = ∅
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.ofDual_intermediateFieldEquivSubgroup_apply : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : FiniteDimensional F E] [inst_4 : IsGalois F E] (K : IntermediateField F E),
  OrderDual.ofDual (IsGalois.intermediateFieldEquivSubgroup K) = K.fixingSubgroup
-- Mathlib.Data.PNat.Factors
PrimeMultiset.toPNatMultiset_ofPNatList : ∀ {l : List ℕ+} (hl : ∀ p ∈ l, p.Prime), (PrimeMultiset.ofPNatList l hl).toPNatMultiset = ↑l
-- Mathlib.Data.Set.Finite.Lattice
Set.Finite.biUnion : ∀ {α : Type u} {ι : Type u_1} {s : Set ι}, s.Finite → ∀ {t : ι → Set α}, (∀ i ∈ s, (t i).Finite) → (⋃ i ∈ s, t i).Finite
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
/-- The tensor of a family of linear maps from `Eᵢ` to `E'ᵢ`, as a continuous multilinear map of
the family.  -/
PiTensorProduct.mapLMultilinear : {ι : Type u_1} →
  [inst : Fintype ι] →
    (𝕜 : Type u_2) →
      (E : ι → Type u_3) →
        [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] →
              (E' : ι → Type u_5) →
                [inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)] →
                  [inst_5 : (i : ι) → NormedSpace 𝕜 (E' i)] →
                    ContinuousMultilinearMap 𝕜 (fun i => E i →L[𝕜] E' i)
                      ((PiTensorProduct 𝕜 fun i => E i) →L[𝕜] PiTensorProduct 𝕜 fun i => E' i)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.lt_of_le_of_ne : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LE a b → a ≠ b → Std.PRange.UpwardEnumerable.LT a b
-- Mathlib.Order.Bounds.Basic
lowerBounds_mono_mem : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} ⦃a b : α⦄, b ≤ a → a ∈ lowerBounds s → b ∈ lowerBounds s
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
AlgebraicGeometry.UniversallyInjective.iff_diagonal : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.UniversallyInjective f ↔ AlgebraicGeometry.Surjective (CategoryTheory.Limits.pullback.diagonal f)
-- Init.Data.BitVec.Bitblast
BitVec.sshiftRightRec.eq_1 : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y 0 = x.sshiftRight' (y &&& BitVec.twoPow w₂ 0)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.HasOrthogonalProjection.ofCompleteSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [CompleteSpace ↥K], K.HasOrthogonalProjection
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.toSubsemigroup_inj : ∀ {M : Type u_1} [inst : AddZeroClass M] {s t : AddSubmonoid M}, s.toAddSubsemigroup = t.toAddSubsemigroup ↔ s = t
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Priority.toInt? : Aesop.Frontend.Priority → Option ℤ
-- Mathlib.Data.FunLike.IsApply
/-- `IsIntCastApply F α` states for all `n : ℤ` and `x : α`, `(n : F) x = n • x`.  -/
IsIntCastApply : (F : Type u_1) → (α : outParam (Type u_2)) → [FunLike F α α] → [IntCast F] → [SMul ℤ α] → Prop
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_map : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k fallback : α},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.map f m).getKeyD k fallback = m.getKeyD k fallback
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [Std.LawfulEqCmp cmp]
  [inst : Std.TransCmp cmp] {k : α}, k ∈ t.keys ↔ k ∈ t
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.instLift : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [inst : AlgebraicGeometry.IsOpenImmersion f]
  (H' : Set.range ⇑g ⊆ Set.range ⇑f) [AlgebraicGeometry.IsOpenImmersion g],
  AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.IsOpenImmersion.lift f g H')
-- Init.Data.List.Sort.Impl
/-- Split a list in two equal parts, reversing the first part.
If the length is odd, the second part will be one element longer.
 -/
List.MergeSort.Internal.splitRevInTwo' : {α : Type u_1} → {n : ℕ} → { l // l.length = n } → { l // l.length = n / 2 } × { l // l.length = (n + 1) / 2 }
-- Mathlib.Order.Directed
/-- If `f` is monotone, `g` is antitone, and `f ≤ g`, then for all `a`, `b` we have `f a ≤ g b`.  -/
Monotone.forall_le_of_antitone : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [IsDirectedOrder α] [inst_2 : Preorder β] {f g : α → β},
  Monotone f → Antitone g → f ≤ g → ∀ (m n : α), f m ≤ g n
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.pos_denom : ∀ (x : ℝ), 0 < expNegInvGlue x + expNegInvGlue (1 - x)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyLT_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h' : ∃ a ∈ t₁, cmp a k = Ordering.lt} (h : t₁.Equiv t₂), t₁.getKeyLT k h' = t₂.getKeyLT k ⋯
-- Init.Data.Range.Polymorphic.PRange
Std.Roi.HasRcoIntersection.mk : {α : Type w} → (Std.Roi α → Std.Rco α → Std.Rco α) → Std.Roi.HasRcoIntersection α
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.mapDomainLinearMap_comp : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {O : Type u_5} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (f : M → N) (g : N → O),
  AddMonoidAlgebra.mapDomainLinearMap R S (g ∘ f) =
    AddMonoidAlgebra.mapDomainLinearMap R S g ∘ₗ AddMonoidAlgebra.mapDomainLinearMap R S f
-- Mathlib.Data.List.AList
AList.lookup_eq_none : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s : AList β}, AList.lookup a s = none ↔ a ∉ s
-- Mathlib.RingTheory.Valuation.AlgebraInstances
ValuationSubring.integralClosure_algebraMap_injective : ∀ {K : Type u_1} [inst : Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) (L : Type u_2) [inst_1 : Field L]
  [inst_2 : Algebra K L],
  Function.Injective ⇑(algebraMap ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L))
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.ringEquivFixedPoints.congr_simp : ∀ (G : Type u_1) (A : Type u_2) (B : Type u_4) [inst : Group G] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra A B] [inst_4 : MulSemiringAction G B] [hA : IsGaloisGroup G A B] [inst_5 : FaithfulSMul A B],
  IsGaloisGroup.ringEquivFixedPoints G A B = IsGaloisGroup.ringEquivFixedPoints G A B
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
Subalgebra.range_isScalarTower_toAlgHom : ∀ (R : Type u) (A : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A), (↑(IsScalarTower.toAlgHom R (↥S) A)).range = Subalgebra.toSubmodule S
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.mk : Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
  Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Lean.Elab.Tactic.TacticParsedSnapshot
-- Mathlib.Algebra.GroupWithZero.ULift
ULift.commGroupWithZero : {α : Type u} → [CommGroupWithZero α] → CommGroupWithZero (ULift.{u_1, u} α)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.findM?_eq_findM?_toList : ∀ {α β : Type} {m : Type → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α Id β] [inst_2 : Std.IteratorLoop α Id m]
  [LawfulMonad m] [Std.Iterators.Finite α Id] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β}
  {f : β → m (ULift.{0, 0} Bool)}, it.findM? f = List.findM? (fun x => ULift.down <$> f x) it.toList
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.coe_copy : ∀ {M : Type u_4} {N : Type u_5} {x : AddZero M} {x_1 : AddZero N} (f : M →+ N) (f' : M → N) (h : f' = ⇑f),
  ⇑(f.copy f' h) = f'
-- Init.Try
/-- `∎` (typed as `\qed`) is a macro that expands to `try?` in tactic mode.  -/
«tactic∎» : Lean.ParserDescr
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.instInhabitedCfg.default : Turing.ToPartrec.Cfg
-- Mathlib.Order.Filter.Bases.Basic
/-- The sequence of sets is antitone.  -/
Filter.IsAntitoneBasis.antitone : ∀ {α : Type u_1} {ι'' : Type u_6} [inst : Preorder ι''] {s'' : ι'' → Set α}, Filter.IsAntitoneBasis s'' → Antitone s''
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.map_obj_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} {U : CategoryTheory.Over X},
  ((CategoryTheory.Over.map f).obj U).left = U.left
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Asymptotics.isEquivalent_nat_ceil : ∀ {R : Type u_1} [inst : NormedField R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [OrderTopology R]
  [inst_4 : FloorRing R], Asymptotics.IsEquivalent Filter.atTop (fun x => ↑⌈x⌉₊) fun x => x
-- Init.Data.SInt.Lemmas
UInt64.ofBitVec_int64ToBitVec : ∀ (x : Int64), { toBitVec := x.toBitVec } = x.toUInt64
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.instIsRightKanExtensionPointwiseRightKanExtensionPointwiseRightKanExtensionCounit : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [inst_3 : L.HasPointwiseRightKanExtension F],
  (L.pointwiseRightKanExtension F).IsRightKanExtension (L.pointwiseRightKanExtensionCounit F)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.instReprHeapNode : {α : Type u_1} → [Repr α] → Repr (Batteries.BinomialHeap.Imp.HeapNode α)
-- Mathlib.Order.DirectedInverseSystem
/-- The setoid on the sigma type defining the direct limit.  -/
DirectLimit.setoid : {ι : Type u_1} →
  [inst : Preorder ι] →
    {F : ι → Type u_4} →
      {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} →
        (f : (i j : ι) → (h : i ≤ j) → T h) →
          [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] →
            [DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] → [IsDirectedOrder ι] → Setoid ((i : ι) × F i)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ \ m₂).getKey? k = m₁.getKey? k
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
/-- If a function is `C^n`, with `1 ≤ n`, then its bundled derivative is continuous.  -/
ContMDiff.continuous_tangentMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} [Is : IsManifold I 1 M]
  [I's : IsManifold I' 1 M'], ContMDiff I I' n f → 1 ≤ n → Continuous (tangentMap I I' f)
-- Mathlib.Algebra.Quaternion
Quaternion.coe_mul_eq_smul : ∀ {R : Type u_3} [inst : CommRing R] (r : R) (a : Quaternion R), ↑r * a = r • a
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.mk_zero_smul : ∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddZeroClass ι] [inst_1 : GradedMonoid.GMul A] {i : ι} (a : A 0) (b : A i),
  GradedMonoid.mk i (a • b) = GradedMonoid.mk 0 a * GradedMonoid.mk i b
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.vcomp_left : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b : B} {f g h : CategoryTheory.FreeBicategory.Hom a b} (η₁ η₂ : CategoryTheory.FreeBicategory.Hom₂ f g)
  (θ : CategoryTheory.FreeBicategory.Hom₂ g h) (a_1 : CategoryTheory.FreeBicategory.Rel η₁ η₂),
  CategoryTheory.FreeBicategory.Rel.below a_1 → motive η₁ η₂ a_1 → CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_iff_nat_mul_le' : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, f' =o[l] g ↔ ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f' x‖ ≤ ‖g x‖
-- Lean.Meta.Tactic.Grind.Types
/-- Returns extensionality theorems for the given type if available.
If `Config.ext` is `false`, the result is `#[]`.
 -/
Lean.Meta.Grind.getExtTheorems : Lean.Expr → Lean.Meta.Grind.GoalM (Array Lean.Meta.Ext.ExtTheorem)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.lift_aleph0 : Cardinal.lift.{u_1, u_2} Cardinal.aleph0 = Cardinal.aleph0
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.instInhabited : {C : Type u} → [inst : CategoryTheory.Groupoid C] → Inhabited (CategoryTheory.Subgroupoid C)
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.semilatticeInf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Limits.HasPullbacks C] → {B : C} → SemilatticeInf (CategoryTheory.Subobject B)
-- Mathlib.Analysis.MeanInequalities
Real.Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg : ∀ {ι : Type u} {f g : ι → ℝ} {p q r : ℝ},
  p.HolderTriple q r →
    (∀ (i : ι), 0 ≤ f i) →
      (∀ (i : ι), 0 ≤ g i) →
        (Summable fun i => f i ^ p) →
          (Summable fun i => g i ^ q) →
            ∑' (i : ι), (f i * g i) ^ r ≤ (∑' (i : ι), f i ^ p) ^ (r / p) * (∑' (i : ι), g i ^ q) ^ (r / q)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_filter_eq_size_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → Bool},
  (Std.TreeMap.filter f t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) t[k] = true
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- The function `n ↦ Λ n / n`, restricted to non-primes in a residue class, is summable.
This is used to convert results on `ArithmeticFunction.vonMangoldt.residueClass` to results
on primes in an arithmetic progression.  -/
ArithmeticFunction.vonMangoldt.summable_residueClass_non_primes_div : ∀ {q : ℕ} (a : ZMod q),
  Summable fun n => (if Nat.Prime n then 0 else ArithmeticFunction.vonMangoldt.residueClass a n) / ↑n
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Submodule.orthogonalComplement_eq_orthogonalComplement : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K L : Submodule 𝕜 E} [K.HasOrthogonalProjection] [L.HasOrthogonalProjection], Kᗮ = Lᗮ ↔ K = L
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.add_compat_left : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {a b c : FreeAlgebra.Pre R X}
  (a_1 : FreeAlgebra.Rel R X a b), FreeAlgebra.Rel.below a_1 → motive a b a_1 → FreeAlgebra.Rel.below ⋯
-- Mathlib.FieldTheory.IsAlgClosed.Classification
/-- Two uncountable algebraically closed fields are isomorphic
if they have the same cardinality and the same characteristic.  -/
IsAlgClosed.ringEquiv_of_equiv_of_char_eq : ∀ {K : Type u} {L : Type v} [inst : Field K] [inst_1 : Field L] [IsAlgClosed K] [IsAlgClosed L] (p : ℕ) [CharP K p]
  [CharP L p], Cardinal.aleph0 < Cardinal.mk K → Nonempty (K ≃ L) → Nonempty (K ≃+* L)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Adding a vector in the direction to a point in the subspace produces a point in the
subspace.  -/
AffineSubspace.vadd_mem_of_mem_direction : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {v : V}, v ∈ s.direction → ∀ {p : P}, p ∈ s → v +ᵥ p ∈ s
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.mono_of_cofan_isVanKampen : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] {ι : Type u_3}
  {F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} {c : CategoryTheory.Limits.Cocone F},
  CategoryTheory.IsVanKampenColimit c → ∀ (i : CategoryTheory.Discrete ι), CategoryTheory.Mono (c.ι.app i)
-- Mathlib.Geometry.Convex.Cone.Pointed
ConvexCone.toPointedCone_top : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E], ⊤.toPointedCone trivial = ⊤