mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- Consider a function `f : α × β → γ`. Suppose that it is continuous on each “vertical fiber”
`{a} × t`, `a ∈ s`, and is Lipschitz continuous on each “horizontal fiber” `s × {b}`, `b ∈ t`
with the same Lipschitz constant `K`. Then it is continuous on `s × t`. Moreover, it suffices
to require continuity on vertical fibers for `a` from a subset `s' ⊆ s` that is dense in `s`.

The actual statement uses (Lipschitz) continuity of `fun y ↦ f (a, y)` and `fun x ↦ f (x, b)`
instead of continuity of `f` on subsets of the product space.  -/
continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : PseudoEMetricSpace γ] (f : α × β → γ) {s s' : Set α} {t : Set β},
  s' ⊆ s →
    s ⊆ closure s' →
      ∀ (K : NNReal),
        (∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t) →
          (∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s) → ContinuousOn f (s ×ˢ t)
-- Mathlib.Algebra.CharP.Reduced
frobenius_inj : ∀ (R : Type u_1) [inst : CommRing R] [IsReduced R] (p : ℕ) [inst_2 : ExpChar R p], Function.Injective ⇑(frobenius R p)
-- Mathlib.Topology.Sets.VietorisTopology
/-- The Vietoris topology on the powerset of a topological space, generated by sets of the form
`{A | A ⊆ U}` and `{A | A ∩ U ≠ ∅}`, where `U` is an open subset of the underlying space. Used for
defining the topologies on `Compacts` and `NonemptyCompacts`.  -/
TopologicalSpace.vietoris : (α : Type u_1) → [TopologicalSpace α] → TopologicalSpace (Set α)
-- Mathlib.CategoryTheory.Opposites
/-- The double opposite category is equivalent to the original.  -/
CategoryTheory.opOpEquivalence : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → Cᵒᵖᵒᵖ ≌ C
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, k ∉ t₂ → (t₁ ∩ t₂).getKey! k = default
-- Aesop.Rule
Aesop.instLTUnsafeRuleInfo : LT Aesop.UnsafeRuleInfo
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCompletionOptions.fromJson : Lean.Json → Except String Lean.Lsp.CompletionOptions
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.isBoundedUnder_le : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {l : Filter α} {c : F},
  (f =O[l] fun _x => c) → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f)
-- Mathlib.Data.Bool.Basic
Bool.bool_iff_false : ∀ {b : Bool}, ¬b = true ↔ b = false
-- Mathlib.MeasureTheory.Constructions.SubmoduleQuotient
Submodule.Quotient.instMeasurableSpaceQuotient : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {p : Submodule R M} → [MeasurableSpace M] → MeasurableSpace (M ⧸ p)
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.cond_pos_of_inter_ne_zero : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s t : Set Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasurableSet s → μ (s ∩ t) ≠ 0 → 0 < μ[t | s]
-- Mathlib.Analysis.Convex.Independent
/-- A convex independent family is injective.  -/
ConvexIndependent.injective : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {p : ι → E}, ConvexIndependent 𝕜 p → Function.Injective p
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.SameKeys.below : {α : Type u} →
  {β : α → Type v} →
    {β' : α → Type u_1} →
      {motive :
          (a : Std.DTreeMap.Internal.Impl α β) → (a_1 : Std.DTreeMap.Internal.Impl α β') → a.SameKeys a_1 → Prop} →
        {a : Std.DTreeMap.Internal.Impl α β} → {a_1 : Std.DTreeMap.Internal.Impl α β'} → a.SameKeys a_1 → Prop
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.instInhabited : {M : Type u_1} → [Inhabited M] → Inhabited (ArchimedeanOrder M)
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.IsExtensionBy_trans_left : ∀ {aig : Std.Sat.AIG ℕ} {new1 : ℕ} {hnew1 : new1 < aig.decls.size} {new2 : ℕ} {hnew2 : new2 < aig.decls.size}
  (state1 state2 state3 : Std.Sat.AIG.toCNF.State✝ aig),
  Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state1 state2 new1 hnew1 →
    Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state2 state3 new2 hnew2 →
      Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state1 state3 new1 hnew1
-- Mathlib.Algebra.Group.Defs
LeftCancelMonoid.toLeftCancelSemigroup : {M : Type u} → [self : LeftCancelMonoid M] → LeftCancelSemigroup M
-- Mathlib.Data.ENNReal.Basic
ENNReal.iUnion_Ioc_coe_nat : ∀ {a : ENNReal}, ⋃ n, Set.Ioc a ↑n = Set.Ioi a \ {⊤}
-- Mathlib.Algebra.Lie.Engel
LieAlgebra.isEngelian_of_subsingleton : ∀ {R : Type u₁} {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [Subsingleton L],
  LieAlgebra.IsEngelian R L
-- Mathlib.SetTheory.ZFC.Class
Class.instMembership : Membership Class.{u_1} Class.{u_1}
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.op_f : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (a : ι),
  e.op.f a = e.f a
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The fraction `s /ₒ 1` as a unit in `R[S⁻¹]`, where `s : S`.  -/
OreLocalization.numeratorUnit : {R : Type u_1} →
  [inst : Monoid R] → {S : Submonoid R} → [inst_1 : OreLocalization.OreSet S] → ↥S → (OreLocalization S R)ˣ
-- Lean.DocString.Markdown
/-- A renderer for custom block elements of type `α`. It receives renderers for inline and block
content, the custom element, and the element's fallback content.
 -/
Lean.Doc.BlockMdRendererOf : Type → Type
-- Mathlib.Combinatorics.SetFamily.HarrisKleitman
IsLowerSet.memberSubfamily : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {a : α},
  IsLowerSet ↑𝒜 → IsLowerSet ↑(Finset.memberSubfamily a 𝒜)
-- Mathlib.Probability.Process.Adapted
MeasureTheory.isStronglyProgressive_const : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {β : Type u_3} [inst_1 : TopologicalSpace β]
  [inst_2 : MeasurableSpace ι] (f : MeasureTheory.Filtration ι m) (b : β),
  MeasureTheory.IsStronglyProgressive f fun x x_1 => b
-- Mathlib.Data.List.AList
/-- Insert a key-value pair into an association list and erase any existing pair
with the same key.  -/
AList.insert : {α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → β a → AList β → AList β
-- Lean.Data.Lsp.Internal
Lean.Lsp.instInhabitedRefIdent.default : Lean.Lsp.RefIdent
-- Mathlib.Analysis.Calculus.Implicit
/-- The point at which `leftFun` and `rightFun` are strictly differentiable  -/
ImplicitFunctionData.pt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [inst_3 : CompleteSpace E] →
            {F : Type u_3} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : CompleteSpace F] →
                    {G : Type u_4} →
                      [inst_7 : NormedAddCommGroup G] →
                        [inst_8 : NormedSpace 𝕜 G] → [inst_9 : CompleteSpace G] → ImplicitFunctionData 𝕜 E F G → E
-- Mathlib.Order.Filter.CountableInter
Filter.mem_ofCountableUnion : ∀ {α : Type u_2} {l : Set (Set α)} {hunion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l}
  {hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l} {s : Set α}, s ∈ Filter.ofCountableUnion l hunion hmono ↔ sᶜ ∈ l
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.instHasLimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C],
  CategoryTheory.Limits.HasLimits (CategoryTheory.CosimplicialObject C)
-- Mathlib.NumberTheory.ModularForms.Cusps
surjective_cosetToCuspOrbit : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)) [inst : 𝒢.IsArithmetic], Function.Surjective (cosetToCuspOrbit 𝒢)
-- Mathlib.Data.Set.Basic
Set.subset_eq_empty : ∀ {α : Type u} {s t : Set α}, t ⊆ s → s = ∅ → t = ∅
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getEntry?_eq_getEntry? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [instBEq : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α β}, t.Ordered → t.getEntry? k = Std.Internal.List.getEntry? k t.toListModel
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.FreeMonoidal.εIso_hom_one : ∀ (R : Type u) [inst : CommRing R],
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.FreeMonoidal.εIso R).hom) 1 = ModuleCat.freeMk PUnit.unit
-- Mathlib.Analysis.Complex.IntegerCompl
/-- **Alias** of `Complex.add_intCast_mem_integerComplement`. -/
Complex.integerComplement.add_coe_int_mem : ∀ {x : ℂ} (a : ℤ), x + ↑a ∈ Complex.integerComplement ↔ x ∈ Complex.integerComplement
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson.eq_3 : ∀ {R : Type u_1} [inst : CommRing R] (k : ℕ) (a : R) (n : ℕ),
  Polynomial.dickson k a n.succ.succ =
    Polynomial.X * Polynomial.dickson k a (n + 1) - Polynomial.C a * Polynomial.dickson k a n
-- Batteries.Data.UnionFind.Basic
/-- Rank of node  -/
Batteries.UFNode.rank : Batteries.UFNode → ℕ
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.mem_iSup_of_mem : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_4} {S : ι → Submonoid M} (i : ι) {x : M}, x ∈ S i → x ∈ iSup S
-- Lean.Data.Lsp.Basic
/-- Represents a reference to a client editor command.

NOTE: No specific commands are specified by LSP, hence
possible commands need to be announced as capabilities.

[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#command)
 -/
Lean.Lsp.Command : Type
-- Mathlib.Data.Set.Lattice
Set.subset_iInter : ∀ {β : Type u_2} {ι : Sort u_5} {t : Set β} {s : ι → Set β}, (∀ (i : ι), t ⊆ s i) → t ⊆ ⋂ i, s i
-- Mathlib.Topology.EMetricSpace.BoundedVariation
_private.Mathlib.Topology.EMetricSpace.BoundedVariation.0.BoundedVariationOn.of_finset : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_3} [inst_1 : PseudoMetricSpace E] (f : α → E) (s : Finset α),
  BoundedVariationOn f ↑s
-- Init.Data.List.ToArray
Array.findIdx.eq_1 : ∀ {α : Type u} (p : α → Bool) (as : Array α), Array.findIdx p as = (Array.findIdx? p as).getD as.size
-- Mathlib.Topology.MetricSpace.Algebra
IsBoundedSMul.dist_pair_smul' : ∀ {α : Type u_1} {β : Type u_2} {inst : PseudoMetricSpace α} {inst_1 : PseudoMetricSpace β} {inst_2 : Zero α}
  {inst_3 : Zero β} {inst_4 : SMul α β} [self : IsBoundedSMul α β] (x₁ x₂ : α) (y : β),
  dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
ContinuousLinearMap.continuousMultilinearMapOption.eq_1 : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {F : Type u_1} {G : Type u_2}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedAddCommGroup G] [inst_7 : NormedSpace 𝕜 G]
  (B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F),
  B.continuousMultilinearMapOption =
    { toFun := fun p => (B (p none).1) fun i => (p (some i)).2 i, map_update_add' := ⋯,
          map_update_smul' := ⋯ }.mkContinuous
      ‖B‖ ⋯
-- Mathlib.Data.Seq.Computation
/-- bind over a function mapping `α` to a `Computation`  -/
Computation.Bind.f : {α : Type u} → {β : Type v} → (α → Computation β) → Computation α ⊕ Computation β → β ⊕ Computation α ⊕ Computation β
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.mem_closure_iff_infEDist_zero`.

---

A point belongs to the closure of `s` iff its infimum edistance to this set vanishes  -/
EMetric.mem_closure_iff_infEdist_zero : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α}, x ∈ closure s ↔ Metric.infEDist x s = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {combined lw rw : ℕ}
  (lhs : aig.RefVec lw) (rhs : aig.RefVec rw) (h : combined = rw + lw) (lw_1 rw_1 : ℕ) (lhs_1 : aig.RefVec lw_1)
  (rhs_1 : aig.RefVec rw_1) (h_1 : combined = rw_1 + lw_1),
  ({ lw := lw, rw := rw, lhs := lhs, rhs := rhs, h := h } =
      { lw := lw_1, rw := rw_1, lhs := lhs_1, rhs := rhs_1, h := h_1 }) =
    (lw = lw_1 ∧ rw = rw_1 ∧ lhs ≍ lhs_1 ∧ rhs ≍ rhs_1)
-- Mathlib.Data.Int.ModEq
Int.ext_ediv_modEq : ∀ {n a b : ℤ}, a / n = b / n → a ≡ b [ZMOD n] → a = b
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.mk.sizeOf_spec : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : SizeOf R] [inst_9 : SizeOf S]
  [inst_10 : SizeOf R'] [inst_11 : SizeOf S'] (toRingHom : P.Ring →+* P'.Ring)
  (toRingHom_algebraMap :
    ∀ (x : R), toRingHom ((algebraMap R P.Ring) x) = (algebraMap R' P'.Ring) ((algebraMap R R') x))
  (algebraMap_toRingHom :
    ∀ (x : P.Ring), (algebraMap P'.Ring S') (toRingHom x) = (algebraMap S S') ((algebraMap P.Ring S) x)),
  sizeOf
      { toRingHom := toRingHom, toRingHom_algebraMap := toRingHom_algebraMap,
        algebraMap_toRingHom := algebraMap_toRingHom } =
    1 + sizeOf toRingHom
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
CategoryTheory.Sieve.generateSingleton_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : Y ⟶ X),
  CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton f) = CategoryTheory.Sieve.generateSingleton f
-- Init.Meta.Defs
Lean.TSyntax.instCoeConsSyntaxNodeKindNil : {k : Lean.SyntaxNodeKind} → {ks : List Lean.SyntaxNodeKind} → Coe (Lean.TSyntax k) (Lean.TSyntax (k :: ks))
-- Mathlib.Data.Set.Countable
Set.enumerateCountable.eq_1 : ∀ {α : Type u} {s : Set α} (h : s.Countable) (default : α) (n : ℕ),
  Set.enumerateCountable h default n =
    match Encodable.decode n with
    | some y => ↑y
    | none => default
-- Init.MetaTypes
Lean.Meta.DSimp.Config.mk.injEq : ∀ (zeta beta eta : Bool) (etaStruct : Lean.Meta.EtaStructMode)
  (iota proj decide autoUnfold failIfUnchanged unfoldPartialApp zetaDelta index zetaUnused zetaHave locals instances
    zeta_1 beta_1 eta_1 : Bool)
  (etaStruct_1 : Lean.Meta.EtaStructMode)
  (iota_1 proj_1 decide_1 autoUnfold_1 failIfUnchanged_1 unfoldPartialApp_1 zetaDelta_1 index_1 zetaUnused_1 zetaHave_1
    locals_1 instances_1 : Bool),
  ({ zeta := zeta, beta := beta, eta := eta, etaStruct := etaStruct, iota := iota, proj := proj, decide := decide,
        autoUnfold := autoUnfold, failIfUnchanged := failIfUnchanged, unfoldPartialApp := unfoldPartialApp,
        zetaDelta := zetaDelta, index := index, zetaUnused := zetaUnused, zetaHave := zetaHave, locals := locals,
        instances := instances } =
      { zeta := zeta_1, beta := beta_1, eta := eta_1, etaStruct := etaStruct_1, iota := iota_1, proj := proj_1,
        decide := decide_1, autoUnfold := autoUnfold_1, failIfUnchanged := failIfUnchanged_1,
        unfoldPartialApp := unfoldPartialApp_1, zetaDelta := zetaDelta_1, index := index_1, zetaUnused := zetaUnused_1,
        zetaHave := zetaHave_1, locals := locals_1, instances := instances_1 }) =
    (zeta = zeta_1 ∧
      beta = beta_1 ∧
        eta = eta_1 ∧
          etaStruct = etaStruct_1 ∧
            iota = iota_1 ∧
              proj = proj_1 ∧
                decide = decide_1 ∧
                  autoUnfold = autoUnfold_1 ∧
                    failIfUnchanged = failIfUnchanged_1 ∧
                      unfoldPartialApp = unfoldPartialApp_1 ∧
                        zetaDelta = zetaDelta_1 ∧
                          index = index_1 ∧
                            zetaUnused = zetaUnused_1 ∧
                              zetaHave = zetaHave_1 ∧ locals = locals_1 ∧ instances = instances_1)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
/-- The inclusion of a submodule into the ambient presheaf of modules.  -/
PresheafOfModules.Submodule.ι : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → {M : PresheafOfModules R} → (N : M.Submodule) → N.toPresheafOfModules ⟶ M
-- Mathlib.RingTheory.Ideal.Operations
Ideal.pow_eq_zero_of_mem : ∀ {R : Type u} [inst : Semiring R] {I : Ideal R} {n m : ℕ}, I ^ n = 0 → n ≤ m → ∀ {x : R}, x ∈ I → x ^ m = 0
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.const.congr_simp : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f f_1 : M),
  f = f_1 →
    ∀ (g g_1 : R) (e_g : g = g_1) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
      (hu : U ≤ PrimeSpectrum.basicOpen g),
      AlgebraicGeometry.StructureSheaf.const f g U hu = AlgebraicGeometry.StructureSheaf.const f_1 g_1 U ⋯
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Face maps for a simplicial object.  -/
CategoryTheory.SimplicialObject.δ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.SimplicialObject C) →
      {n : ℕ} → Fin (n + 2) → (X.obj (Opposite.op { len := n + 1 }) ⟶ X.obj (Opposite.op { len := n }))
-- Mathlib.Topology.UniformSpace.HeineCantor
/-- Heine-Cantor: a continuous function on a compact set of a uniform space is uniformly
continuous.  -/
IsCompact.uniformContinuousOn_of_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {s : Set α} {f : α → β},
  IsCompact s → ContinuousOn f s → UniformContinuousOn f s
-- Std.Time.Date.Unit.Week
Std.Time.Week.OfYear.instReprOrdinal : Repr Std.Time.Week.OfYear.Ordinal
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- Bialgebra equivalences are symmetric.  -/
BialgEquiv.symm : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → (A ≃ₐc[R] B) → B ≃ₐc[R] A
-- Mathlib.Data.Set.Function
Set.InvOn.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {p : Set γ} {f : α → β} {g : β → γ} {f' : β → α}
  {g' : γ → β},
  Set.InvOn f' f s t → Set.InvOn g' g t p → Set.MapsTo f s t → Set.MapsTo g' p t → Set.InvOn (f' ∘ g') (g ∘ f) s p
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.prun_congr : ∀ {m : Type w → Type w'} {α : Type u} {β : Type w} [inst : Monad m] [LawfulMonad m] {x y : Std.Iterators.HetT m α}
  {f : (a : α) → x.Property a → m β} (h : x = y), x.prun f = y.prun fun a ha => f a ⋯
-- Mathlib.Algebra.Ring.Subring.IntPolynomial
Polynomial.int_natDegree : ∀ {K : Type u_1} [inst : Field K] (R : Subring K) (P : Polynomial K) (hP : ∀ (n : ℕ), P.coeff n ∈ R),
  (Polynomial.int R P hP).natDegree = P.natDegree
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- The cusps of `SL(2, ℤ)` are precisely the elements of `ℙ¹(ℚ)`.  -/
isCusp_SL2Z_iff : ∀ {c : OnePoint ℝ}, IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range ↔ c ∈ Set.range (OnePoint.map Rat.cast)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.hasEigenvalue_iff_mem_spectrum : ∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {f : Module.End K V} {μ : K}, f.HasEigenvalue μ ↔ μ ∈ spectrum K f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k fallback : α},
      k ∉ m → l.contains k = false → (m.insertManyIfNewUnit l).getKeyD k fallback = fallback
-- Init.Data.Array.Lemmas
Array.foldl_eq_foldr_reverse : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : β → α → β} {b : β},
  Array.foldl f b xs = Array.foldr (fun x y => f y x) b xs.reverse
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
/-- Given a `ContinuousFunctionalCalculus S A q`. If we form the predicate `p` for `a : A`
characterized by: `q a` and the spectrum of `a` restricts to the scalar subring `R` via
`f : C(S, R)`, then we can get a restricted functional calculus
`ContinuousFunctionalCalculus R A p`.  -/
SpectrumRestricts.closedEmbeddingCFC : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {p q : A → Prop} [inst : Semifield R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Semifield S]
  [inst_6 : StarRing S] [inst_7 : MetricSpace S] [inst_8 : IsTopologicalSemiring S] [inst_9 : ContinuousStar S]
  [inst_10 : Ring A] [inst_11 : StarRing A] [inst_12 : Algebra S A] [inst_13 : Algebra R S] [inst_14 : Algebra R A]
  [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] [inst_18 : TopologicalSpace A]
  [ClosedEmbeddingContinuousFunctionalCalculus S A q] [ContinuousMap.UniqueHom R A] [CompleteSpace R] (f : C(S, R)),
  IsUniformEmbedding ⇑(algebraMap R S) →
    p 0 → (∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f) → ClosedEmbeddingContinuousFunctionalCalculus R A p
-- Mathlib.Data.Set.Basic
Set.left_eq_inter : ∀ {α : Type u} {s t : Set α}, s = s ∩ t ↔ s ⊆ t
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_of_lt_of_le_one : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b c : α}, b < c → a ≤ 1 → b * a < c
-- Mathlib.Algebra.Group.Defs
CommMagma.mk : {G : Type u} → [toMul : Mul G] → (∀ (a b : G), a * b = b * a) → CommMagma G
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- The "main pair" for an algebra `(A, α)` is the pair of morphisms `(F α, ε_FA)`. It is always a
reflexive pair, and will be used to construct the left adjoint to the comparison functor and show it
is an equivalence.
 -/
CategoryTheory.Monad.MonadicityInternal.main_pair_reflexive : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra),
  CategoryTheory.IsReflexivePair (F.map A.a) (adj.counit.app (F.obj A.A))
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- The comparison `Σ cᵢ*xᵢ R 0`.  -/
Mathlib.Tactic.Linarith.PComp.c : Mathlib.Tactic.Linarith.PComp → Mathlib.Tactic.Linarith.Comp
-- Init.Data.String.Defs
String.singleton_eq_ofList : ∀ {c : Char}, String.singleton c = String.ofList [c]
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.append.injEq : ∀ {l r w : ℕ} (lhs : Std.Tactic.BVDecide.BVExpr l) (rhs : Std.Tactic.BVDecide.BVExpr r) (h : w = l + r) (l_1 r_1 : ℕ)
  (lhs_1 : Std.Tactic.BVDecide.BVExpr l_1) (rhs_1 : Std.Tactic.BVDecide.BVExpr r_1) (h_1 : w = l_1 + r_1),
  (lhs.append rhs h = lhs_1.append rhs_1 h_1) = (l = l_1 ∧ r = r_1 ∧ lhs ≍ lhs_1 ∧ rhs ≍ rhs_1)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.rangeKerLift_injective : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (φ : G →+ H),
  Function.Injective ⇑(QuotientAddGroup.rangeKerLift φ)
-- Mathlib.Data.NNReal.Defs
NNReal.coe_two : ↑2 = 2
-- Std.Data.Internal.List.Associative
Std.Internal.List.Prod.fst_comp_toSigma : ∀ {α : Type u} {β : Type v}, Sigma.fst ∘ Std.Internal.List.Prod.toSigma = Prod.fst
-- Lean.LocalContext
Lean.LocalContext.instForInLocalDeclOfMonad : {m : Type u_1 → Type u_2} → [Monad m] → ForIn m Lean.LocalContext Lean.LocalDecl
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBase.spanning : ∀ {α : Type u_2} {M : Matroid α} {B : Set α}, M.IsBase B → M.Spanning B
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- A `ℂ`-basis of `ℂ^n` that is also a `ℤ`-basis of the `integerLattice`.  -/
NumberField.canonicalEmbedding.latticeBasis : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      Module.Basis (Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)) ℂ ((K →+* ℂ) → ℂ)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_union_Ioo' : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c d : α},
  c < b → a < d → Set.Ioo a b ∪ Set.Ioo c d = Set.Ioo (min a c) (max b d)