mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.NormNum.Eq
Mathlib.Meta.NormNum.isInt_eq_false : ∀ {α : Type u_1} [inst : Ring α] [CharZero α] {a b : α} {a' b' : ℤ},
  Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → decide (a' = b') = false → ¬a = b
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.InfinitePos.neg : ∀ {x : ℝ*}, x.InfinitePos → (-x).InfiniteNeg
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.entryAtIdx!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited ((a : α) × β a)] {i : ℕ}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.entryAtIdx! i = t₂.entryAtIdx! i
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
/-- Given an immersion `f : X ⟶ Y`, this is the biggest open set `U ⊆ Y` containing the image of `X`
such that `X` is closed in `U`.
 -/
AlgebraicGeometry.Scheme.Hom.coborderRange : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → [AlgebraicGeometry.IsImmersion f] → Y.Opens
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The isomorphism `K.cycles i ≅ L.cycles i` induced by an isomorphism
in `HomologicalComplex`.  -/
HomologicalComplex.cyclesMapIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {K L : HomologicalComplex C c} →
            (K ≅ L) → (i : ι) → [inst_2 : K.HasHomology i] → [inst_3 : L.HasHomology i] → K.cycles i ≅ L.cycles i
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c) (n : ι),
  (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K).X.X n = (K.X n).X
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.fintypeMul.eq_1 : ∀ {α : Type u_2} [inst : Mul α] [inst_1 : DecidableEq α] (s t : Set α) [inst_2 : Fintype ↑s] [inst_3 : Fintype ↑t],
  s.fintypeMul t = Set.fintypeImage2 (fun x1 x2 => x1 * x2) s t
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃))
  {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  (hom :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j))
  (i₁ i₂ i₃ : ι),
  CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
    CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (hom i₁ i₃) (sq₃ i₁ i₂ i₃).p₁₃ (sq₃ i₁ i₂ i₃).p₁
      (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.DiagramState.mk : String → Std.HashMap String (String × ProofWidgets.Html) → ProofWidgets.Penrose.DiagramState
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.prod_top : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (K : Subgroup G),
  K.prod ⊤ = Subgroup.comap (MonoidHom.fst G N) K
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapEmbedding_isBase_iff : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α ↪ β} {B : Set β},
  (M.mapEmbedding f).IsBase B ↔ M.IsBase (⇑f ⁻¹' B) ∧ B ⊆ Set.range ⇑f
-- Mathlib.Analysis.Complex.Trigonometric
Complex.enorm_exp_ofReal_mul_I : ∀ (x : ℝ), ‖Complex.exp (↑x * Complex.I)‖ₑ = 1
-- Std.Do.Internal.Ensures.Lemmas
/-- An `ErasesTo`-witnessed refinement `x` of `y` recovers `y` by projecting out the property.  -/
Std.Do.Internal.ErasesTo.map_eq : ∀ {α : Type u} {m : Type u → Type v} {P : α → Prop} {x : m { b // P b }} {y : m α} [inst : Monad m] [LawfulMonad m],
  Std.Do.Internal.ErasesTo x y → Subtype.val <$> x = y
-- Init.Data.SInt.Bitwise
Int8.xor_self : ∀ {a : Int8}, a ^^^ a = 0
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.singletonSubgraph_adj : ∀ {V : Type u} (G : SimpleGraph V) (v a a_1 : V), (G.singletonSubgraph v).Adj a a_1 = ⊥ a a_1
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Filter.Eventually.exists_measurable_mem : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : Filter α} [f.IsMeasurablyGenerated] {p : α → Prop},
  (∀ᶠ (x : α) in f, p x) → ∃ s ∈ f, MeasurableSet s ∧ ∀ x ∈ s, p x
-- Mathlib.Algebra.Ring.Defs
Ring.toZSMul : {R : Type u} → [self : Ring R] → ZSMul R
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.mk.sizeOf_spec : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} [inst : SizeOf ι] [inst_1 : SizeOf ι']
  (f : ι → ι') (injective_f : Function.Injective f) (rel : ∀ {i₁ i₂ : ι}, c.Rel i₁ i₂ → c'.Rel (f i₁) (f i₂)),
  sizeOf { f := f, injective_f := injective_f, rel := rel } = 1
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.tendsto_iterate_efixedPoint' : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsComplete s)
  (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s)
  (hx : edist x (f x) ≠ ⊤),
  Filter.Tendsto (fun n => f^[n] x) Filter.atTop (nhds (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx))
-- Mathlib.NumberTheory.Dioph
Dioph.diophFn_comp2 : ∀ {α : Type} {f g : (α → ℕ) → ℕ},
  Dioph.DiophFn f →
    Dioph.DiophFn g →
      ∀ {h : ℕ → ℕ → ℕ},
        (Dioph.DiophFn fun v => h (v (Fin2.ofNat' 0)) (v (Fin2.ofNat' 1))) → Dioph.DiophFn fun v => h (f v) (g v)
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.list_prod_ofFn_eq_dProd : ∀ {ι : Type u_1} {A : ι → Type u_3} [inst : AddMonoid ι] [inst_1 : GradedMonoid.GMonoid A] {n : ℕ}
  (f : Fin n → GradedMonoid A),
  (List.ofFn f).prod =
    GradedMonoid.mk ((List.finRange n).dProdIndex fun i => (f i).fst)
      ((List.finRange n).dProd (fun i => (f i).fst) fun i => (f i).snd)
-- Init.Data.Fin.Lemmas
Fin.succ_le_succ_iff : ∀ {n : ℕ} {a b : Fin n}, a.succ ≤ b.succ ↔ a ≤ b
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_prod_of_nonempty : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β},
  (s ×ˢ t).Nonempty → (MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t)
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.isEqSome.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → α → Sort u_2) (x : α) (h_1 : (a b : α) → motive (some a) b)
  (h_2 : (x : α) → motive none x),
  (match none, x with
    | some a, b => h_1 a b
    | none, x => h_2 x) =
    h_2 x
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.zero : {α : Type u} → [inst : Lean.Grind.NatModule α] → Lean.Grind.IntModule.OfNatModule.Q α
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.ServerInfo.mk.inj : ∀ {name : String} {version? : Option String} {name_1 : String} {version?_1 : Option String},
  { name := name, version? := version? } = { name := name_1, version? := version?_1 } →
    name = name_1 ∧ version? = version?_1
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeIsoAux_hom_app : ∀ (C : Type u) (X : CategoryTheory.FreeMonoidalCategory C)
  (X_1 : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C),
  (CategoryTheory.FreeMonoidalCategory.normalizeIsoAux C X).hom.app X_1 =
    (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C X X_1).hom
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mulSingle_mul : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → MulOneClass (G i)] [inst_3 : ∀ (i : ι), OneMemClass (S i) (G i)]
  [inst_4 : ∀ (i : ι), MulMemClass (S i) (G i)] (i : ι) (r s : G i),
  RestrictedProduct.mulSingle A i (r * s) = RestrictedProduct.mulSingle A i r * RestrictedProduct.mulSingle A i s
-- Mathlib.Data.Multiset.Range
Multiset.range_subset : ∀ {m n : ℕ}, Multiset.range m ⊆ Multiset.range n ↔ m ≤ n
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.comap_map_comap : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  {S : L.Substructure N} {f : L.Hom M N},
  FirstOrder.Language.Substructure.comap f
      (FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f S)) =
    FirstOrder.Language.Substructure.comap f S
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_alterKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
  {l : List ((a : α) × β a)},
  (Std.Internal.List.alterKey k f l).isEmpty =
    ((l.isEmpty || l.length == 1 && Std.Internal.List.containsKey k l) &&
      (f (Std.Internal.List.getValueCast? k l)).isNone)
-- Mathlib.Analysis.SpecialFunctions.Exp
Complex.continuous_exp : Continuous Complex.exp
-- Mathlib.Algebra.Ring.CharZero
Function.mulSupport_natCast : ∀ {α : Type u_1} {R : Type u_2} {n : ℕ} [inst : AddMonoidWithOne R] [CharZero R],
  n ≠ 1 → Function.mulSupport ↑n = Set.univ
-- Init.Data.Range.Polymorphic.Lemmas
Std.PRange.UpwardEnumerable.exists_of_succ_le : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LE (Std.PRange.succ a) b →
    ∃ b', b = Std.PRange.succ b' ∧ Std.PRange.UpwardEnumerable.LE a b'
-- Mathlib.Computability.TuringDegree
TuringEquivalent.symm : ∀ {f g : ℕ →. ℕ}, TuringEquivalent f g → TuringEquivalent g f
-- Lean.Meta.Tactic.Simp.Rewrite
_private.Lean.Meta.Tactic.Simp.Rewrite.0.Lean.Meta.Simp.rewrite?.inErasedSet : Lean.PHashSet Lean.Meta.Origin → Lean.Meta.SimpTheorem → Bool
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β k}, (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ k ∉ m then some k else m.getKey? a
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.rightAngleRotation_trans_neg_orientation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)), (-o).rightAngleRotation = o.rightAngleRotation.trans (LinearIsometryEquiv.neg ℝ)
-- Mathlib.RingTheory.Flat.EquationalCriterion
/-- **Equational criterion for flatness**, backward direction.

If every relation $\sum_i f_i x_i = 0$ in $M$ is trivial, then $M$ is flat.  -/
Module.Flat.of_forall_isTrivialRelation : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → Module.IsTrivialRelation f x) → Module.Flat R M
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy-Goursat theorem** for a disk: if `f : ℂ → E` is continuous on a closed disk
`{z | ‖z - c‖ ≤ R}` and is complex differentiable on the open disk,
then the integral $\oint_{|z-c|=R}f(z)\,dz$ equals zero.  -/
DiffContOnCl.circleIntegral_eq_zero : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ},
  0 ≤ R → ∀ {f : ℂ → E} {c : ℂ}, DiffContOnCl ℂ f (Metric.ball c R) → ∮ (z : ℂ) in C(c, R), f z = 0
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.image_eq_preimage_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X),
  ⇑h '' s = ⇑h.symm ⁻¹' s
-- Mathlib.Analysis.Normed.Group.Defs
/-- An enormed commutative monoid is an additive commutative monoid
endowed with a continuous enorm which is positive definite.

We don't have `ENormedAddCommMonoid` extend `EMetricSpace`, since the canonical instance `ℝ≥0∞`
is not an `EMetricSpace`. This is because `ℝ≥0∞` carries the order topology, which is distinct from
the topology coming from `edist`.  -/
ENormedAddCommMonoid : (E : Type u_8) → [TopologicalSpace E] → Type u_8
-- Mathlib.Algebra.Algebra.Subalgebra.Directed
Subalgebra.isMulCommutative_iSup : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {ι : Type u_4}
  [Nonempty ι] {S : ι → Subalgebra R A} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)],
  Directed (fun x1 x2 => x1 ≤ x2) S → IsMulCommutative ↥(⨆ i, S i)
-- Init.Data.Slice.Array.Lemmas
Array.stop_mkSlice_rii : ∀ {α : Type u_1} {xs : Array α}, (Std.Rii.Sliceable.mkSlice xs *...*).stop = xs.size
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
_private.Lean.Meta.Tactic.Simp.Arith.Int.Basic.0.Int.Internal.Linear.Poly.denoteExpr.go : (ℕ → Lean.Expr) → Lean.Expr → Int.Internal.Linear.Poly → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.Localization.BaseChange
LocalizedModule.equivTensorProduct_apply_mk : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (x : M) (s : ↥S),
  (LocalizedModule.equivTensorProduct S M) (LocalizedModule.mk x s) = Localization.mk 1 s ⊗ₜ[R] x
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.nonUnitalRing : (α : Type u) → [Semigroup α] → NonUnitalRing (FreeAbelianGroup α)
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.eLpNorm_le_eLpNorm_of_exponent_le : ∀ {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ε}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {p q : ENNReal},
  p ≤ q →
    ∀ [MeasureTheory.IsProbabilityMeasure μ],
      MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm f q μ
-- Mathlib.Algebra.Quandle
ShelfHom.instFunLike : {S₁ : Type u_1} → {S₂ : Type u_2} → [inst : Shelf S₁] → [inst_1 : Shelf S₂] → FunLike (ShelfHom S₁ S₂) S₁ S₂
-- Mathlib.CategoryTheory.Monoidal.Discrete
/-- The monoidal natural isomorphism corresponding to
composing two additive morphisms.  -/
CategoryTheory.Discrete.addMonoidalFunctorComp : {M : Type u} →
  [inst : AddMonoid M] →
    {N : Type u'} →
      [inst_1 : AddMonoid N] →
        {K : Type u} →
          [inst_2 : AddMonoid K] →
            (F : M →+ N) →
              (G : N →+ K) →
                (CategoryTheory.Discrete.addMonoidalFunctor F).comp (CategoryTheory.Discrete.addMonoidalFunctor G) ≅
                  CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
IsIdempotentElem.finite_quasispectrum : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : Module 𝕜 A] [IsScalarTower 𝕜 A A]
  [SMulCommClass 𝕜 A A] {p : A}, IsIdempotentElem p → (quasispectrum 𝕜 p).Finite
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toArray.go.match_1.eq_2 : ∀ {α β : 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 β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (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 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', 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, property⟩ => h_3 property) =
    h_2 it' h
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.not_isUnit_X_add_C : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] (a : R), ¬IsUnit (Polynomial.X + Polynomial.C a)
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
CategoryTheory.Idempotents.DoldKan.equivalence_counitIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.Idempotents.DoldKan.equivalence.counitIso = CategoryTheory.Idempotents.DoldKan.η
-- Mathlib.Topology.MetricSpace.Closeds
/-- `NonemptyCompacts α` inherits a metric space structure, as the Hausdorff
edistance between two such sets is finite.  -/
Metric.NonemptyCompacts.instMetricSpace : {α : Type u_1} → [inst : MetricSpace α] → MetricSpace (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.Topology.MetricSpace.Thickening
Metric.diam_thickening_le : ∀ {ε : ℝ} {α : Type u_2} [inst : PseudoMetricSpace α] (s : Set α),
  0 ≤ ε → Metric.diam (Metric.thickening ε s) ≤ Metric.diam s + 2 * ε
-- Mathlib.Analysis.Meromorphic.Basic
/-- Finite products of meromorphic functions are meromorphic.  -/
MeromorphicAt.fun_prod : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {ι : Type u_5} {s : Finset ι} {F : ι → 𝕜 → 𝕜'} {x : 𝕜},
  (∀ σ ∈ s, MeromorphicAt (F σ) x) → MeromorphicAt (fun z => ∏ n ∈ s, F n z) x
-- Lean.Elab.DeclModifiers
Lean.Elab.ComputeKind.meta.sizeOf_spec : sizeOf Lean.Elab.ComputeKind.meta = 1
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.mul_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A]
  (a b : DoubleCentralizer 𝕜 A), (a * b).toProd.2 = b.toProd.2 * a.toProd.2
-- Lean.Meta.ReduceEval
Lean.Meta.instReduceEvalString : Lean.Meta.ReduceEval String
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isEmpty_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  (Std.DHashMap.Const.ofList l).isEmpty = l.isEmpty
-- Init.Data.List.Lemmas
List.length_insert : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {l : List α},
  (List.insert a l).length = l.length + if a ∈ l then 0 else 1
-- Std.Data.HashSet.Basic
/-- Monadically computes a value by folding the given function over the elements in the hash set in some
order.
 -/
Std.HashSet.foldM : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} → {m : Type v → Type w} → [Monad m] → {β : Type v} → (β → α → m β) → β → Std.HashSet α → m β
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.Hom.mk.injEq : ∀ {R : Type u} [inst : CommRing R] {V W : CoalgCat R}
  (toCoalgHom' toCoalgHom'_1 : ↑V.toModuleCat →ₗc[R] ↑W.toModuleCat),
  ({ toCoalgHom' := toCoalgHom' } = { toCoalgHom' := toCoalgHom'_1 }) = (toCoalgHom' = toCoalgHom'_1)
-- Mathlib.Testing.Plausible.Functions
_private.Mathlib.Testing.Plausible.Functions.0.Plausible.TotalFunction.zeroDefault.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Plausible.TotalFunction α β → Sort u_3) (A : List ((_ : α) × β)) (a : β)
  (h_1 : (A : List ((_ : α) × β)) → (a : β) → motive (Plausible.TotalFunction.withDefault A a)),
  (match Plausible.TotalFunction.withDefault A a with
    | Plausible.TotalFunction.withDefault A a => h_1 A a) =
    h_1 A a
-- Mathlib.Algebra.Polynomial.Splits
/-- **Alias** of `Polynomial.Splits.of_degree_le_one_of_invertible`. -/
Polynomial.splits_of_degree_le_one_of_invertible : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.degree ≤ 1 → ∀ (h : Invertible f.leadingCoeff), f.Splits
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.memL1_limitProcess_densityProcess : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β},
      MeasurableSet s →
        MeasureTheory.MemLp
          (MeasureTheory.Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s)
            (ProbabilityTheory.countableFiltration γ) (ν a))
          1 (ν a)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Multiset.aestronglyMeasurable_fun_sum : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [ContinuousAdd M] (s : Multiset (α → M)),
  (∀ f ∈ s, MeasureTheory.AEStronglyMeasurable f μ) →
    MeasureTheory.AEStronglyMeasurable (fun x => (Multiset.map (fun f => f x) s).sum) μ
-- Std.Net.Addr
/-- Try to parse `s` as an IPv6 address according to
[RFC 2373](https://datatracker.ietf.org/doc/html/rfc2373), returning `none` on failure.
 -/
Std.Net.IPv6Addr.ofString : String → Option Std.Net.IPv6Addr
-- Mathlib.Topology.Connected.LocallyPathConnected
connectedComponentSetoid_eq_pathSetoid : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X], connectedComponentSetoid X = pathSetoid X
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.instCompleteSpace : ∀ {α : Type u} [inst : UniformSpace α], CompleteSpace (CauchyFilter α)
-- Mathlib.Algebra.Group.Basic
eq_mul_inv_iff_mul_eq : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a = b * c⁻¹ ↔ a * c = b
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property `P` of ring homs satisfies `RingHom.HoldsForLocalization`
if `P` holds for each localization map `R →+* M⁻¹R`.  -/
RingHom.HoldsForLocalization : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.NumberTheory.SumFourSquares
/-- **Euler's four-square identity**.  -/
euler_four_squares : ∀ {R : Type u_1} [inst : CommRing R] (a b c d x y z w : R),
  (a * x - b * y - c * z - d * w) ^ 2 + (a * y + b * x + c * w - d * z) ^ 2 + (a * z - b * w + c * x + d * y) ^ 2 +
      (a * w + b * z - c * y + d * x) ^ 2 =
    (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2)
-- Init.Data.Nat.Lcm
Nat.lcm_mul_left_dvd_mul_lcm : ∀ (k m n : ℕ), (m * n).lcm k ∣ m.lcm k * n.lcm k
-- Init.Data.String.Lemmas.Hashable
String.Slice.hash_eq : ∀ {s : String.Slice}, hash s = s.copy.hash
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.maximumClique_exists : ∀ {α : Type u_3} {G : SimpleGraph α} [inst : Finite α], ∃ s, G.IsMaximumClique s
-- Mathlib.Algebra.Ring.TransferInstance
/-- Transfer `Ring` across an `Equiv`  -/
Equiv.ring : {α : Type u_1} → {β : Type u_2} → α ≃ β → [Ring β] → Ring α
-- Mathlib.GroupTheory.Nilpotent
/-- A p-group is nilpotent  -/
IsPGroup.isNilpotent : ∀ {G : Type u_1} [hG : Group G] [Finite G] {p : ℕ} [hp : Fact (Nat.Prime p)], IsPGroup p G → Group.IsNilpotent G
-- Mathlib.Algebra.Order.Monoid.Basic
OrderEmbedding.addRight.eq_1 : ∀ {α : Type u_2} [inst : Add α] [inst_1 : LinearOrder α] [inst_2 : AddRightStrictMono α] (m : α),
  OrderEmbedding.addRight m = OrderEmbedding.ofStrictMono (fun n => n + m) ⋯
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_ne_nil_iff : ∀ {m n : ℕ}, (m<...n).toArray ≠ #[] ↔ m + 1 < n
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
_private.Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno.0.Fin.succ.match_1.splitter : {n : ℕ} → (motive : Fin n → Sort u_1) → (x : Fin n) → ((i : ℕ) → (h : i < n) → motive ⟨i, h⟩) → motive x
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PrepathObject.RightHomotopy.trans_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} {P : HomotopicalAlgebra.PrepathObject Y} {X : C}
  {f₀ f₁ f₂ : X ⟶ Y} (h : P.RightHomotopy f₀ f₁) {P' : HomotopicalAlgebra.PrepathObject Y} (h' : P'.RightHomotopy f₁ f₂)
  [inst_1 : CategoryTheory.Limits.HasPullback P.p₁ P'.p₀],
  (h.trans h').h = CategoryTheory.Limits.pullback.lift h.h h'.h ⋯