mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.Hom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Comon C} (hom : M.X ⟶ N.X) [isComonHom_hom : CategoryTheory.IsComonHom hom] (hom_1 : M.X ⟶ N.X)
  (isComonHom_hom_1 : CategoryTheory.IsComonHom hom_1),
  ({ hom := hom, isComonHom_hom := isComonHom_hom } = { hom := hom_1, isComonHom_hom := isComonHom_hom_1 }) =
    (hom = hom_1)
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.lt_omega0_opow_succ : ∀ {a b : Ordinal.{u_1}}, a < Ordinal.omega0 ^ Order.succ b ↔ ∃ n, a < Ordinal.omega0 ^ b * ↑n
-- Mathlib.Logic.Unique
Pi.default_apply : ∀ {α : Sort u_1} {β : α → Sort v} [inst : (a : α) → Inhabited (β a)] (a : α), default a = default
-- Lean.Syntax
Lean.Syntax.setAtomVal : Lean.Syntax → String → Lean.Syntax
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.coe_id : ∀ (α : Type u_2) [inst : TopologicalSpace α] [inst_1 : Preorder α], ⇑(ContinuousOrderHom.id α) = id
-- Mathlib.MeasureTheory.Constructions.SimpleGraph
SimpleGraph.instMeasurableSpace : {V : Type u_1} → MeasurableSpace (SimpleGraph V)
-- Mathlib.Algebra.Tropical.Lattice
instSemilatticeSupTropical : {R : Type u_1} → [SemilatticeSup R] → SemilatticeSup (Tropical R)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.cellFrontier.eq_1 : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n),
  Topology.RelCWComplex.cellFrontier n i = ↑(Topology.RelCWComplex.map n i) '' Metric.sphere 0 1
-- Std.Async.Basic
/-- Converts `Except` to `BaseAsync`.
 -/
Std.Async.BaseAsync.ofExcept : {α : Type} → Except Empty α → Std.Async.BaseAsync α
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- The evaluation functors jointly reflect colimits: that is, to show a cocone is a colimit of `F`
it suffices to show that each evaluation cocone is a colimit. In other words, to prove a cocone is
colimiting you can show it's pointwise colimiting.
 -/
CategoryTheory.Limits.evaluationJointlyReflectsColimits : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              (c : CategoryTheory.Limits.Cocone F) →
                ((k : K) → CategoryTheory.Limits.IsColimit (((CategoryTheory.evaluation K C).obj k).mapCocone c)) →
                  CategoryTheory.Limits.IsColimit c
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.isReflection_conj_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w t : W),
  cs.IsReflection (w * t * w⁻¹) ↔ cs.IsReflection t
-- Mathlib.Algebra.Ring.Int.Units
Int.units_eq_one_or : ∀ (u : ℤˣ), u = 1 ∨ u = -1
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.FG.restrictScalars : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : Semiring A] [inst_4 : Module R A] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] {S : Submodule A M}
  [Module.Finite R A], S.FG → (Submodule.restrictScalars R S).FG
-- Lean.Parser.Extension
Lean.Parser.registerAliasCore : {α : Type} → IO.Ref (Lean.Parser.AliasTable α) → Lean.Name → Lean.Parser.AliasValue α → IO Unit
-- Mathlib.Data.Rat.Defs
Rat.num_ne_zero : ∀ {q : ℚ}, q.num ≠ 0 ↔ q ≠ 0
-- Mathlib.Tactic.MoveAdd
/-- `pairUp L R` takes two lists `L R : List Expr` as inputs.
It scans the elements of `L`, looking for a corresponding `DefEq` `Expr`ession in `R`.
If it finds one such element `d`, then it sets the element `d : R` aside, removing it from `R`, and
it continues with the matching on the remainder of `L` and on `R.erase d`.

At the end, it returns the sublist of `R` of the elements that were matched to some element of `L`,
in the order in which they appeared in `L`,
as well as the sublist of `L` of elements that were not matched, also in the order in which they
appeared in `L`.

Example:
```lean
#eval do
  let L := [mkNatLit 0, (← mkFreshExprMVar (some (mkConst ``Nat))), mkNatLit 0] -- i.e. [0, _, 0]
  let R := [mkNatLit 0, mkNatLit 0,                                 mkNatLit 1] -- i.e. [0, 1]
  dbg_trace f!"{(← pairUp L R)}"
/- output:
`([0, 0], [0])`
the output LHS list `[0, 0]` consists of the first `0` and the `MVarId`.
the output RHS list `[0]` corresponds to the last `0` in `L`.
-/
```
 -/
Mathlib.MoveAdd.pairUp : List (Lean.Expr × Bool × Lean.Syntax) →
  List Lean.Expr → Lean.MetaM (List (Lean.Expr × Bool) × List (Lean.Expr × Bool × Lean.Syntax))
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPoly.beq : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Bool
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateOsetImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu →
    Lean.FVarId → ℕ → Lean.Compiler.LCNF.Arg pu → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.Order.Interval.Basic
NonemptyInterval.ext_iff : ∀ {α : Type u_6} {inst : LE α} {x y : NonemptyInterval α}, x = y ↔ x.toProd = y.toProd
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_neg : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (x : K),
  ArchimedeanClass.stdPart (-x) = -ArchimedeanClass.stdPart x
-- Mathlib.RingTheory.LaurentSeries
/-- Laurent Series with coefficients in a field are complete w.r.t. the `X`-adic valuation  -/
LaurentSeries.instLaurentSeriesComplete : ∀ {K : Type u_2} [inst : Field K], CompleteSpace (LaurentSeries K)
-- Std.Internal.Do.PredTrans
/-- `Monad` instance for `PredTrans`: `pure` returns the postcondition applied to the value,
and `bind` threads the postcondition through the continuation.  -/
Std.Internal.Do.instMonadPredTrans : (Pred : Type u) → (EPred : Type v) → Monad (Std.Internal.Do.PredTrans Pred EPred)
-- Lean.Environment
Lean.Kernel.Exception.alreadyDeclared : Lean.Kernel.Environment → Lean.Name → Lean.Kernel.Exception
-- Mathlib.Order.Filter.Pointwise
Filter.nonpos_iff : ∀ {α : Type u_2} [inst : Zero α] {f : Filter α}, f ≤ 0 ↔ 0 ∈ f
-- Mathlib.Order.Atoms
Pi.isAtom_iff_eq_single : ∀ {ι : Type u_4} {π : ι → Type u} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (π i)]
  [inst_2 : (i : ι) → OrderBot (π i)] {f : (i : ι) → π i}, IsAtom f ↔ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_le_aleph_ofNat : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Cardinal.lift.{v, u} c ≤ Cardinal.aleph (OfNat.ofNat n) ↔ c ≤ Cardinal.aleph (OfNat.ofNat n)
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- If the codomain of an injective linear map is finite dimensional, the domain must be as well.  -/
FiniteDimensional.of_injective : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂),
  Function.Injective ⇑f → ∀ [FiniteDimensional K V₂], FiniteDimensional K V
-- Init.Data.Order.Ord
Array.instOrientedCmpCompareLex : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.OrientedCmp cmp], Std.OrientedCmp (Array.compareLex cmp)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.nhds_eq_inf_comap : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {z : Z},
  z ∈ e.source → nhds z = Filter.comap proj (nhds (proj z)) ⊓ Filter.comap (Prod.snd ∘ ↑e) (nhds (↑e z).2)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_op_iff_unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] (Q : CategoryTheory.ObjectProperty Cᵒᵖ),
  Q.IsClosedUnderColimitsOfShape Jᵒᵖ ↔ Q.unop.IsClosedUnderLimitsOfShape J
-- Lean.Data.Lsp.Basic
Lean.Lsp.instHashableMarkupKind.hash : Lean.Lsp.MarkupKind → UInt64
-- Mathlib.Analysis.Convex.PathConnected
/-- A convex set is preconnected.  -/
Convex.isPreconnected : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E] {s : Set E}, Convex ℝ s → IsPreconnected s
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- **Alias** of `AddMonoidAlgebra.le_inf_support_coeff_add`. -/
AddMonoidAlgebra.le_inf_support_add : ∀ {R : Type u_1} {A : Type u_3} {T : Type u_4} [inst : SemilatticeInf T] [inst_1 : OrderTop T] [inst_2 : Semiring R]
  (degt : A → T) (f g : AddMonoidAlgebra R A),
  f.coeff.support.inf degt ⊓ g.coeff.support.inf degt ≤ (f + g).coeff.support.inf degt
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- A morphism in `D` is a morphism of `A`-module objects if it commutes with
the action maps  -/
CategoryTheory.IsModHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            (A : C) →
              [inst_4 : CategoryTheory.MonObj A] →
                {M N : D} → [CategoryTheory.ModObj A M] → [CategoryTheory.ModObj A N] → (M ⟶ N) → Prop
-- Init.Data.Vector.Zip
Vector.map_uncurry_zip_eq_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α → β → γ} {as : Vector α n} {bs : Vector β n},
  Vector.map (Function.uncurry f) (as.zip bs) = Vector.zipWith f as bs
-- Mathlib.Algebra.Ring.Ext
NonUnitalSemiring.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : NonUnitalSemiring R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
-- Mathlib.Dynamics.Flow
/-- Every flow is a factor of itself.  -/
Flow.IsFactorOf.self : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α), ϕ.IsFactorOf ϕ
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.eraseMany_eq_eraseListₘ_toListModel : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m m₂ : Std.DHashMap.Internal.Raw₀ α β),
  ↑(m.eraseManyEntries ↑m₂) = m.eraseListₘ (List.map (fun x => x.fst) (Std.DHashMap.Internal.toListModel (↑m₂).buckets))
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.mk_coe : ∀ (z : Complex.UnitClosedDisc) (hz : optParam (‖↑z‖ ≤ 1) ⋯), Complex.UnitClosedDisc.mk (↑z) hz = z
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tan_inv_eq_cot : ∀ (x : ℂ), (Complex.tan x)⁻¹ = x.cot
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Oplax.StrongTrans.Modification η θ)
  {a b : B} {a' : C} (f : a ⟶ b) (g : G.obj b ⟶ a'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft (F.map f) (CategoryTheory.Bicategory.whiskerRight (Γ.app b) g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (θ.app b) g).inv
        (CategoryTheory.Bicategory.whiskerRight (θ.naturality f).hom g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (η.app b) g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom g)
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (Γ.app a) (G.map f)) g))
-- Mathlib.Algebra.Algebra.Opposite
/-- An algebra homomorphism `f : A →ₐ[R] B` such that `f x` commutes with `f y` for all `x, y` defines
an algebra homomorphism from `Aᵐᵒᵖ`.  -/
AlgHom.fromOpposite : {R : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] → (f : A →ₐ[R] B) → (∀ (x y : A), Commute (f x) (f y)) → Aᵐᵒᵖ →ₐ[R] B
-- Mathlib.CategoryTheory.ComposableArrows.Three
CategoryTheory.ComposableArrows.threeδ₂Toδ₁_app_two : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {i j k l : C} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l)
  (f₁₂ : i ⟶ k) (f₂₃ : j ⟶ l) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃),
  (CategoryTheory.ComposableArrows.threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 2 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₂ f₁ f₂₃).obj 2)
-- Init.System.ST
ST.pure : {α σ : Type} → α → ST σ α
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.pathStar_injective : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V),
  (∀ (u : U), Function.Injective (φ.star u)) → ∀ (u : U), Function.Injective (φ.pathStar u)
-- Mathlib.Order.Filter.IndicatorFunction
indicator_union_eventuallyEq : ∀ {α : Type u_1} {M : Type u_3} [inst : AddMonoid M] {s t : Set α} {f : α → M} {l : Filter α},
  (∀ᶠ (a : α) in l, a ∉ s ∩ t) → (s ∪ t).indicator f =ᶠ[l] s.indicator f + t.indicator f
-- Mathlib.Logic.Relation
Relation.ReflTransGen.below.refl : ∀ {α : Type u_1} {r : α → α → Prop} {a : α} {motive : (a_1 : α) → Relation.ReflTransGen r a a_1 → Prop},
  Relation.ReflTransGen.below ⋯
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Option.orElse.match_1.splitter : {α : Type u_1} →
  (motive : Option α → (Unit → Option α) → Sort u_2) →
    (x : Option α) →
      (x_1 : Unit → Option α) →
        ((a : α) → (x : Unit → Option α) → motive (some a) x) → ((b : Unit → Option α) → motive none b) → motive x x_1
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tensorLId_symm_apply : ∀ {R : Type uR} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : AddCommGroup M₂] [inst_2 : Module R M₂]
  [inst_3 : Invertible 2] (Q₂ : QuadraticForm R M₂) (x : M₂), Q₂.tensorLId.symm x = (TensorProduct.lid R M₂).symm x
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.equalizer.condition_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- The `BoxIntegral.IntegrationParams` corresponding to the McShane integral. In the
corresponding filter, we require that the tagged partition is subordinate to a (possibly,
discontinuous) positive function `r`; the tags may be outside of the corresponding closed box
(but still inside the ambient closed box `I.Icc`).  -/
BoxIntegral.IntegrationParams.McShane : BoxIntegral.IntegrationParams
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
/-- The sum of the dimensions of s + t and s ∩ t is the sum of the dimensions of s and t  -/
Submodule.finrank_sup_add_finrank_inf_eq : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (s t : Submodule K V) [FiniteDimensional K ↥s] [FiniteDimensional K ↥t],
  Module.finrank K ↥(s ⊔ t) + Module.finrank K ↥(s ⊓ t) = Module.finrank K ↥s + Module.finrank K ↥t
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate.beq.sizeOf_spec : sizeOf Std.Tactic.BVDecide.Gate.beq = 1
-- Aesop.RuleSet
Aesop.instEmptyCollectionGlobalRuleSet : EmptyCollection Aesop.GlobalRuleSet
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.indefiniteDiagonal_assoc : ∀ (l : Type u_4) (R : Type u₂) [inst : DecidableEq l] [inst_1 : CommRing R] [inst_2 : Fintype l],
  LieAlgebra.Orthogonal.indefiniteDiagonal (Unit ⊕ l) l R =
    (Matrix.reindexLieEquiv (Equiv.sumAssoc Unit l l).symm)
      (Matrix.fromBlocks 1 0 0 (LieAlgebra.Orthogonal.indefiniteDiagonal l l R))
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsRefl.nondegenerate_iff_separatingRight : ∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁] {B : M →ₗ[R] M →ₗ[R] M₁},
  B.IsRefl → (B.Nondegenerate ↔ B.SeparatingRight)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.self_le_maxKey!_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α} {v : β k},
  (compare k (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.maxKey!).isLE = true
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.mulSupport_one_add' : ∀ {ι : Type u_1} {R : Type u_5} [inst : One R] [inst_1 : AddLeftCancelMonoid R] (f : ι → R),
  Function.mulSupport (1 + f) = Function.support f
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- A morphism of Schemes is an open immersion if it is an open immersion as a morphism
of LocallyRingedSpaces
 -/
AlgebraicGeometry.IsOpenImmersion : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme
-- Mathlib.RingTheory.QuasiFinite.Weakly
Algebra.weaklyQuasiFiniteAt_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (q : Ideal S)
  [inst_3 : q.IsPrime],
  Algebra.WeaklyQuasiFiniteAt R q ↔
    Algebra.QuasiFinite R (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- The `eval` map is surjective at `x`.  -/
smoothSheaf.eval_surjective : ∀ {𝕜 : 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] (N : Type u)
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H N] (x : M), Function.Surjective (smoothSheaf.eval IM I N x)
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.mk.inj : ∀ {toPartOrd : PartOrd} {isFintype : Fintype ↑toPartOrd} {toPartOrd_1 : PartOrd} {isFintype_1 : Fintype ↑toPartOrd_1},
  { toPartOrd := toPartOrd, isFintype := isFintype } = { toPartOrd := toPartOrd_1, isFintype := isFintype_1 } →
    toPartOrd = toPartOrd_1 ∧ isFintype ≍ isFintype_1
-- Mathlib.RingTheory.Int.Basic
Int.exists_prime_and_dvd : ∀ {n : ℤ}, n.natAbs ≠ 1 → ∃ p, Prime p ∧ p ∣ n
-- Lean.Parser.Term.Basic
Lean.Parser.Term.optIdent.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Order.LiminfLimsup
isBounded_ge_nhds : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedGENhdsClass α] (a : α),
  Filter.IsBounded (fun x1 x2 => x1 ≥ x2) (nhds a)
-- Mathlib.Topology.Order.WithTop
TopologicalSpace.instOrderTopologyWithBot : ∀ {ι : Type u_1} [inst : Preorder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι], OrderTopology (WithBot ι)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.mk.injEq : ∀ {M : Type u_8} {N : Type u_9} {φ : M → N} {X : Type u_10} [inst : VAdd M X] {Y : Type u_11} [inst_1 : VAdd N Y]
  (toFun : X → Y) (map_vadd' : ∀ (m : M) (x : X), toFun (m +ᵥ x) = φ m +ᵥ toFun x) (toFun_1 : X → Y)
  (map_vadd'_1 : ∀ (m : M) (x : X), toFun_1 (m +ᵥ x) = φ m +ᵥ toFun_1 x),
  ({ toFun := toFun, map_vadd' := map_vadd' } = { toFun := toFun_1, map_vadd' := map_vadd'_1 }) = (toFun = toFun_1)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
stronglyMeasurable_bot_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : TopologicalSpace β] [Nonempty β] [T2Space β],
  MeasureTheory.StronglyMeasurable f ↔ ∃ c, f = fun x => c
-- Mathlib.MeasureTheory.Order.Lattice
OrderDual.instMeasurableInf₂ : ∀ {M : Type u_1} [inst : MeasurableSpace M] [inst_1 : Max M] [MeasurableSup₂ M], MeasurableInf₂ Mᵒᵈ
-- Mathlib.Data.Sym.Basic
Sym.exists_cons_of_mem : ∀ {α : Type u_1} {n : ℕ} {s : Sym α (n + 1)} {a : α}, a ∈ s → ∃ t, s = a ::ₛ t
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddMemClass.toAddSemigroup.eq_1 : ∀ {M : Type u_4} [inst : AddSemigroup M] {A : Type u_5} [inst_1 : SetLike A M] [inst_2 : AddMemClass A M] (S : A),
  AddMemClass.toAddSemigroup S = { toAdd := AddMemClass.add S, add_assoc := ⋯ }
-- Aesop.Rule
Aesop.NormSimpRule.instHashable : Hashable Aesop.NormSimpRule
-- Mathlib.Algebra.Category.Grp.EpiMono
_private.Mathlib.Algebra.Category.Grp.EpiMono.0.GrpCat.SurjectiveOfEpiAuxs.termH : Lean.ParserDescr
-- Mathlib.CategoryTheory.Category.Bipointed
pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun : ∀ (X : Pointed) (a : ((pointedToBipointed.comp bipointedToPointedSnd).obj X).X),
  (pointedToBipointedCompBipointedToPointedSnd.hom.app X).toFun a = a
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Handler is called when its key is a strict prefix of the configuration key.
The matched key may be `Name.anonymous`.  -/
Lean.Elab.ConfigEval.EvalConfigItemHandlerKind.wildcard : Lean.Elab.ConfigEval.EvalConfigItemHandlerKind
-- Lean.Elab.Match
Lean.Elab.Term.precheckMatch : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- An isomorphism of graphs induces a bijection of connected components.  -/
SimpleGraph.Iso.connectedComponentEquiv : {V : Type u} →
  {V' : Type v} → {G : SimpleGraph V} → {G' : SimpleGraph V'} → G ≃g G' → G.ConnectedComponent ≃ G'.ConnectedComponent
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.inv_limsup : ∀ {ι : Type u_4} {x : ι → ENNReal} {l : Filter ι}, (Filter.limsup x l)⁻¹ = Filter.liminf (fun i => (x i)⁻¹) l
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_natCast : ∀ (n : ℕ), (↑n).toReal = ↑n
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegrable_congr_ae : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {g : ℝ → ε},
  f =ᵐ[μ.restrict (Set.uIoc a b)] g → (IntervalIntegrable f μ a b ↔ IntervalIntegrable g μ a b)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_lt_sq_iff₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀}
  [ZeroLEOneClass M₀], 0 ≤ a → (1 < a ^ 2 ↔ 1 < a)
-- Init.Data.Array.MapIdx
Array.mapFinIdx_eq_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β}, xs.mapFinIdx f = #[] ↔ xs = #[]
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.comp_left_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.SimplicialObject.Augmented C}
  (a : X ⟶ Y) (a_1 : Y ⟶ Z) (X_1 : SimplexCategoryᵒᵖ),
  (CategoryTheory.CategoryStruct.comp a a_1).left.app X_1 =
    CategoryTheory.CategoryStruct.comp (a.left.app X_1) (a_1.left.app X_1)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trPosNum.eq_3 : ∀ (n : PosNum), Turing.PartrecToTM2.trPosNum n.bit1 = Turing.PartrecToTM2.Γ'.bit1 :: Turing.PartrecToTM2.trPosNum n
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- **Alias** of `ContinuousOn.continuous_domRestrict_iff_continuous_uniformOnFun`.

---

A family `f : X → α → β`, each of which is continuous on a compact set `s : Set α` is
continuous in the topology `X → α →ᵤ[{s}] β` if and only if the family of continuous restrictions
`X → C(s, β)` is continuous.  -/
ContinuousOn.continuous_restrict_iff_continuous_uniformOnFun : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {X : Type u_1}
  [inst_2 : TopologicalSpace X] {f : X → α → β} {s : Set α} (hf : ∀ (x : X), ContinuousOn (f x) s) [CompactSpace ↑s],
  (Continuous fun x => { toFun := s.domRestrict (f x), continuous_toFun := ⋯ }) ↔
    Continuous fun x => (UniformOnFun.ofFun {s}) (f x)