mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.RamificationInertia.Unramified
IsUnramifiedAt.of_liesOver_of_ne_bot : ∀ (R : Type u_1) {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [IsScalarTower R S T] (p : Ideal S) (P : Ideal T)
  [P.LiesOver p] [inst_8 : p.IsPrime] [inst_9 : P.IsPrime] [Algebra.IsUnramifiedAt R P] [Algebra.EssFiniteType R S]
  [Algebra.EssFiniteType R T] [IsDedekindDomain S],
  P.primeCompl ≤ nonZeroDivisors T → (p ≠ ⊥ → P ≠ ⊥) → Algebra.IsUnramifiedAt R p
-- Mathlib.Logic.Encodable.Basic
PUnit.encodable : Encodable PUnit.{u_3 + 1}
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.kernelForkBiproductToSubtype_cone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {K : Type}
  [inst_2 : Finite K] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop),
  (CategoryTheory.Limits.kernelForkBiproductToSubtype f p).cone =
    CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.coe_one : ∀ {K : Type u_1} [inst : Field K], (algebraMap (NumberField.RingOfIntegers K) K) ↑1 = 1
-- Mathlib.Order.PartialSups
upperBounds_range_partialSups : ∀ {α : Type u_1} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : Preorder ι] [inst_2 : LocallyFiniteOrderBot ι]
  (f : ι → α), upperBounds (Set.range ⇑(partialSups f)) = upperBounds (Set.range f)
-- Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
PositiveLinearMap.instContinuousLinearMapClassComplexOfLinearMapClassOfOrderHomClass : ∀ {A₁ : Type u_1} {A₂ : Type u_2} [inst : NonUnitalCStarAlgebra A₁] [inst_1 : NonUnitalCStarAlgebra A₂]
  [inst_2 : PartialOrder A₁] [StarOrderedRing A₁] [inst_4 : PartialOrder A₂] [StarOrderedRing A₂] {F : Type u_5}
  [inst_6 : FunLike F A₁ A₂] [LinearMapClass F ℂ A₁ A₂] [OrderHomClass F A₁ A₂], ContinuousLinearMapClass F ℂ A₁ A₂
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- The identity morphism of an algebra of endofunctor `F`  -/
CategoryTheory.Endofunctor.Algebra.Hom.id : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} → (A : CategoryTheory.Endofunctor.Algebra F) → A.Hom A
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftMonoidWithZeroHom_apply_div' : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} [inst_2 : CommGroupWithZero L]
  (φ : Polynomial K →*₀ L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L))
  (p q : Polynomial K),
  (RatFunc.liftMonoidWithZeroHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p) /
      (RatFunc.liftMonoidWithZeroHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) q) =
    φ p / φ q
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.WeakRankFunction.mk.inj : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} {inst : PartialOrder α} {rank : ↑P.II → α}
  {lt : ∀ {x y : ↑P.II}, P.AncestralRel x y → (↑x).dim = (↑y).dim → rank x < rank y} {rank_1 : ↑P.II → α}
  {lt_1 : ∀ {x y : ↑P.II}, P.AncestralRel x y → (↑x).dim = (↑y).dim → rank_1 x < rank_1 y},
  { rank := rank, lt := lt } = { rank := rank_1, lt := lt_1 } → rank = rank_1
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- If one multiplies by `c i` the coordinates in a finset `s`, then the image under a multilinear
map is multiplied by `∏ i ∈ s, c i`. This is mainly an auxiliary statement to prove the result when
`s = univ`, given in `map_smul_univ`, although it can be useful in its own right as it does not
require the index set `ι` to be finite.  -/
MultilinearMap.map_piecewise_smul : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (c : ι → R) (m : (i : ι) → M₁ i)
  (s : Finset ι), f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryEquivClass.toSemilinearEquivClass : ∀ {𝓕 : Type u_11} {R : outParam (Type u_12)} {R₂ : outParam (Type u_13)} {inst : Semiring R} {inst_1 : Semiring R₂}
  {σ₁₂ : outParam (R →+* R₂)} {σ₂₁ : outParam (R₂ →+* R)} {inst_2 : RingHomInvPair σ₁₂ σ₂₁}
  {inst_3 : RingHomInvPair σ₂₁ σ₁₂} {E : outParam (Type u_14)} {E₂ : outParam (Type u_15)}
  {inst_4 : SeminormedAddCommGroup E} {inst_5 : SeminormedAddCommGroup E₂} {inst_6 : Module R E} {inst_7 : Module R₂ E₂}
  {inst_8 : EquivLike 𝓕 E E₂} [self : SemilinearIsometryEquivClass 𝓕 σ₁₂ E E₂], SemilinearEquivClass 𝓕 σ₁₂ E E₂
-- Mathlib.Computability.Reduce
ManyOneEquiv.trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {p : α → Prop} {q : β → Prop} {r : γ → Prop}, ManyOneEquiv p q → ManyOneEquiv q r → ManyOneEquiv p r
-- Init.Data.Int.Gcd
Int.lcm_eq_natAbs_lcm_natAbs : ∀ (m n : ℤ), m.lcm n = m.natAbs.lcm n.natAbs
-- Mathlib.NumberTheory.Transcendental.Liouville.Measure
ae_not_liouvilleWith : ∀ᵐ (x : ℝ), ∀ p > 2, ¬LiouvilleWith p x
-- Mathlib.Data.List.Nodup
List.getElem_bijective_iff : ∀ {α : Type u} {l : List α} [inst : BEq α] [LawfulBEq α],
  (Function.Bijective fun n => l[n]) ↔ ∀ (a : α), List.count a l = 1
-- Aesop.Tree.UnsafeQueue
Aesop.PostponedSafeRule.output : Aesop.PostponedSafeRule → Aesop.RuleTacOutput
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.isPushout_iff_isPushout : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {R' S' : Type u}
  [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S'] [inst_7 : Algebra R' S']
  [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S'],
  CategoryTheory.IsPushout (CommRingCat.ofHom (algebraMap R R')) (CommRingCat.ofHom (algebraMap R S))
      (CommRingCat.ofHom (algebraMap R' S')) (CommRingCat.ofHom (algebraMap S S')) ↔
    Algebra.IsPushout R R' S S'
-- Init.Data.List.Basic
List.filterTR.loop.eq_def : ∀ {α : Type u} (p : α → Bool) (a a_1 : List α),
  List.filterTR.loop p a a_1 =
    match a, a_1 with
    | [], acc => acc.reverse
    | a :: as, acc =>
      match p a with
      | true => List.filterTR.loop p as (a :: acc)
      | false => List.filterTR.loop p as acc
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- Preserving the initial object implies preserving all colimits of the empty diagram.  -/
CategoryTheory.Limits.preservesColimitsOfShape_pempty_of_preservesInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) G
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The object property on `CostructuredArrow L X` induced by a morphism property.  -/
CategoryTheory.MorphismProperty.costructuredArrowObj : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {T : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} T] →
        (L : CategoryTheory.Functor A T) →
          {X : T} →
            CategoryTheory.MorphismProperty T → CategoryTheory.ObjectProperty (CategoryTheory.CostructuredArrow L X)
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ker_toHomUnits : ∀ {G : Type u_1} [inst : Group G] {M : Type u_8} [inst_1 : Monoid M] (f : G →* M), f.toHomUnits.ker = f.ker
-- Mathlib.NumberTheory.SumTwoSquares
/-- The set of natural numbers that are sums of two squares is closed under multiplication.  -/
Nat.sq_add_sq_mul : ∀ {a b x y u v : ℕ}, a = x ^ 2 + y ^ 2 → b = u ^ 2 + v ^ 2 → ∃ r s, a * b = r ^ 2 + s ^ 2
-- Init.Data.AC
Lean.Data.AC.sort.loop.eq_1 : ∀ (a : List ℕ), Lean.Data.AC.sort.loop a [] = a
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iic_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α], LowerSet.Iic ⊤ = ⊤
-- Mathlib.Topology.Connected.Basic
/-- The connected component of `(x, y)` in the product space is the product of the connected
components of `x` and `y`.  -/
connectedComponent_prod : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (x : α) (y : β),
  connectedComponent (x, y) = connectedComponent x ×ˢ connectedComponent y
-- Std.Http.Data.Status
/-- Proof that the reason phrase contains only valid characters.
 -/
Std.Http.CustomStatus.validReasonPhrase : ∀ (self : Std.Http.CustomStatus), Std.Http.IsValidReasonPhrase self.phrase
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
ContDiffAt.cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : E → ℂ} {x : E} {n : WithTop ℕ∞},
  ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n (fun x => Complex.exp (f x)) x
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- Postcomposition of a 1-morphism as a functor from the category of 1-morphisms `b ⟶ c` into the
category of functors `(a ⟶ b) ⥤ (a ⟶ c)`.  -/
CategoryTheory.Bicategory.postcomposing : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    (a b c : B) → CategoryTheory.Functor (b ⟶ c) (CategoryTheory.Functor (a ⟶ b) (a ⟶ c))
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- A function is continuously differentiable up to `n` at a point `x` if, for any integer `k ≤ n`,
there is a neighborhood of `x` where `f` admits derivatives up to order `n`, which are continuous.
The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
number, `∞`, or `ω`.

For `n = ∞`, we only require that this holds up to any finite order (where the neighborhood may
depend on the finite order we consider).
For `n = ω`, we require the function to be analytic at `x`. The precise
definition we give (all the derivatives should be analytic) is more involved to work around issues
when the space is not complete, but it is equivalent when the space is complete.
 -/
ContDiffAt : (𝕜 : Type u) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type uE} →
      [inst_1 : NormedAddCommGroup E] →
        [NormedSpace 𝕜 E] →
          {F : Type uF} → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → WithTop ℕ∞ → (E → F) → E → Prop
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
ergodic_mul_left_iff_denseRange_zpow : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [SecondCountableTopology G] [BorelSpace G] {g : G} (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasure μ]
  [μ.InnerRegular] [μ.IsMulLeftInvariant] [NeZero μ], Ergodic (fun x => g * x) μ ↔ DenseRange fun x => g ^ x
-- Mathlib.NumberTheory.Real.Irrational
irrational_natCast_div_iff : ∀ {n : ℕ} {x : ℝ}, Irrational (↑n / x) ↔ n ≠ 0 ∧ Irrational x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_insert_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k : α} {v : β} {kmi : α}, (t.insert k v).minKey?.get ⋯ = kmi → (cmp kmi k).isLE = true
-- Init.NotationExtra
unexpandSigma : Lean.PrettyPrinter.Unexpander
-- Lean.Server.FileWorker.ExampleHover
_private.Lean.Server.FileWorker.ExampleHover.0.Lean.Server.FileWorker.Hover.RWState : Type
-- Mathlib.Order.Bounds.Basic
isGLB_le_isLUB : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a b : α}, IsGLB s a → IsLUB s b → s.Nonempty → a ≤ b
-- Mathlib.Algebra.CharP.Reduced
/-- If `ringChar R = 2`, where `R` is a finite reduced commutative ring,
then every `a : R` is a square.  -/
isSquare_of_charTwo' : ∀ {R : Type u_1} [Finite R] [inst : CommRing R] [IsReduced R] [CharP R 2] (a : R), IsSquare a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : β → β},
      (t.modify k f).maxKey? = Option.map (fun km => if cmp km k = Ordering.eq then k else km) t.maxKey?
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- The preferred chart at each point  -/
ChartedSpaceCore.chartAt : {H : Type u_5} → [inst : TopologicalSpace H] → {M : Type u_6} → ChartedSpaceCore H M → M → PartialEquiv M H
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.concat_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w x : V} (p : G.Walk u v) (h : G.Adj v w) (q : G.Walk w x),
  (p.concat h).append q = p.append (SimpleGraph.Walk.cons h q)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.distinct_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → List.Pairwise (fun a b => ¬compare a b = Ordering.eq) t.keys
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.evalConvSeqBracketed : Lean.Elab.Tactic.Tactic
-- Mathlib.Analysis.Convex.Segment
openSegment_eq_image_lineMap : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] (x y : E), openSegment 𝕜 x y = ⇑(AffineMap.lineMap x y) '' Set.Ioo 0 1
-- Mathlib.Algebra.Group.Units.Defs
/-- The underlying value in the base `AddMonoid`.  -/
AddUnits.val : {α : Type u} → [inst : AddMonoid α] → AddUnits α → α
-- Mathlib.GroupTheory.Finiteness
AddSubgroup.FG.eq_1 : ∀ {G : Type u_3} [inst : AddGroup G] (P : AddSubgroup G), P.FG = ∃ S, AddSubgroup.closure ↑S = P
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_id_set_eq_sUnion : ∀ {α : Type u_2} (s : Finset (Set α)), s.sup id = ⋃₀ ↑s
-- Mathlib.Topology.UniformSpace.HeineCantor
HasCompactSupport.uniformContinuous_of_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} [inst_2 : Zero β],
  HasCompactSupport f → Continuous f → UniformContinuous f
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.all₂.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (a : α) (as : List α) (b : β) (bs : List β)
  (h_1 : Unit → motive [] []) (h_2 : (a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs))
  (h_3 : (x : List α) → (x_1 : List β) → motive x x_1),
  (match a :: as, b :: bs with
    | [], [] => h_1 ()
    | a :: as, b :: bs => h_2 a as b bs
    | x, x_1 => h_3 x x_1) =
    h_2 a as b bs
-- Mathlib.Topology.Bases
/-- A set is dense iff it has non-trivial intersection with all basis sets.  -/
TopologicalSpace.IsTopologicalBasis.dense_iff : ∀ {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis b → ∀ {s : Set α}, Dense s ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_eq_sdiff_iff_inf_eq_inf : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], y \ x = y \ z ↔ y ⊓ x = y ⊓ z
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.of_mul_left_right : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime (x * y) z → IsCoprime y z
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instIsPurePure : ∀ {φ : Prop} (σs : List (Type u_1)), Std.Do.SPred.Tactic.IsPure ⌜φ⌝ φ
-- Std.Http.Data.Chunk
/-- Creates an `ExtensionName` from a string, panicking with an error message if the string contains
invalid characters or is empty.
 -/
Std.Http.Chunk.ExtensionName.ofString! : String → Std.Http.Chunk.ExtensionName
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.clear_ok : ∀ {p : Turing.PartrecToTM2.Γ' → Bool} {k : Turing.PartrecToTM2.K'} {q : Turing.PartrecToTM2.Λ'}
  {s : Option Turing.PartrecToTM2.Γ'} {L₁ : List Turing.PartrecToTM2.Γ'} {o : Option Turing.PartrecToTM2.Γ'}
  {L₂ : List Turing.PartrecToTM2.Γ'} {S : Turing.PartrecToTM2.K' → List Turing.PartrecToTM2.Γ'},
  Turing.PartrecToTM2.splitAtPred p (S k) = (L₁, o, L₂) →
    StateTransition.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr)
      { l := some (Turing.PartrecToTM2.Λ'.clear p k q), var := s, stk := S }
      { l := some q, var := o, stk := Function.update S k L₂ }
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Presheaf.classifier_Ω : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.Presheaf.classifier C).Ω = CategoryTheory.Functor.sieves C
-- Mathlib.Tactic.Assume
/-- `assume e` introduces a new (unnamed) hypothesis of type `e`.
It is equivalent to `intro (_ : e)`.

The argument `e` is required to be a proposition, definitionally equal to the hypothesis
(or domain of a dependent function) in the goal. The introduced hypothesis will have
the exact form the user wrote.

Example:

```lean
example {α} (f : α → α) (h : Function.Injective f) : ∀ x y, f x = f y → x = y := by
  intro x y
  assume f x = f y
  apply h
  assumption
```
 -/
assume : Lean.ParserDescr
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.toLinearMap_mk' : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (e : V ≃ₗ[A] W) (he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e),
  (↑(Representation.Equiv.mk e he)).toLinearMap = ↑e
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuous_finite : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] [Finite ι]
  {F : ι → X → α}, Equicontinuous F ↔ ∀ (i : ι), Continuous (F i)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.instInhabitedSubtypeMem : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (S : Subalgebra R A) → Inhabited ↥S
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.Limits.HasLimit
    ((CategoryTheory.Limits.cospan f g).comp AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace)
-- Mathlib.Order.SetNotation
Set.mem_iUnion : ∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, x ∈ ⋃ i, s i ↔ ∃ i, x ∈ s i
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.ofHom_hom : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} (f : M ⟶ N),
  SemimoduleCat.ofHom (SemimoduleCat.Hom.hom f) = f
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.isVertexCover_compl : ∀ {V : Type u_1} {G : SimpleGraph V} {c : Set V}, G.IsVertexCover cᶜ ↔ G.IsIndepSet c
-- Mathlib.Data.Set.Finite.Lemmas
Set.exists_max_image : ∀ {α : Type u} {β : Type v} [inst : LinearOrder β] (s : Set α) (f : α → β),
  s.Finite → s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.of_mul_monic_left : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.Monic → (p * q).Monic → q.Monic
-- Mathlib.Analysis.BoxIntegral.UnitPartition
_private.Mathlib.Analysis.BoxIntegral.UnitPartition.0.BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_box_aux₁ : ∀ (n : ℕ) [NeZero n] (x : ℝ) (a : ℤ), ↑a < x ↔ ↑a ≤ (↑⌈↑n * x⌉ - 1) / ↑n
-- Mathlib.Analysis.Polynomial.Order
Polynomial.zero_le_negOnePow_mul_eval_of_le_roots_of_leadingCoeff_nonneg : ∀ {P : Polynomial ℝ} {x : ℝ},
  (∀ (y : ℝ), P.IsRoot y → x ≤ y) → 0 ≤ P.leadingCoeff → 0 ≤ ↑↑(↑P.natDegree).negOnePow * Polynomial.eval x P
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Restrict.isFiniteMeasure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (μ : MeasureTheory.Measure α) [hs : Fact (μ s < ⊤)],
  MeasureTheory.IsFiniteMeasure (μ.restrict s)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β}, List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (m.insertMany l)[k']? = some v
-- Init.Data.Array.GetLit
Array.toListLitAux.congr_simp : ∀ {α : Type u_1} (xs xs_1 : Array α) (e_xs : xs = xs_1) (n n_1 : ℕ) (e_n : n = n_1) (hsz : xs.size = n) (i i_1 : ℕ)
  (e_i : i = i_1) (a : i ≤ xs.size) (a_1 a_2 : List α),
  a_1 = a_2 → xs.toListLitAux n hsz i a a_1 = xs_1.toListLitAux n_1 ⋯ i_1 ⋯ a_2
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.commutator_diag2_transvection : ∀ {F : Type u_1} [inst : Field F] (a : F) (ha : a ≠ 0) (b c : F),
  c = b * (a ^ 2 - 1) →
    ⁅Matrix.SpecialLinearGroup.diag2 a ha, Matrix.SpecialLinearGroup.transvection ⋯ b⁆ =
      Matrix.SpecialLinearGroup.transvection ⋯ c
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Multiset.insert_eq_cons : ∀ {α : Type u_1} (a : α) (s : Multiset α), insert a s = a ::ₘ s
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModuleHierarchyImportsParams.mk.injEq : ∀ (module module_1 : Lean.Lsp.LeanModule), ({ module := module } = { module := module_1 }) = (module = module_1)
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₁₂_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) (X₁ : C₁),
  (CategoryTheory.bifunctorComp₁₂ F₁₂ G).obj X₁ = CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsAtomic.isPrenex : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsAtomic → φ.IsPrenex
-- Mathlib.Algebra.BigOperators.Finprod
AddMonoidHom.map_finsum_Prop : ∀ {M : Type u_2} {N : Type u_3} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {p : Prop} (f : M →+ N) (g : p → M),
  f (∑ᶠ (x : p), g x) = ∑ᶠ (x : p), f (g x)
-- Mathlib.Data.Int.LeastGreatest
/-- If `P : ℤ → Prop` is a predicate such that the set `{m : P m}` is bounded below and nonempty,
then this set has the least element. This lemma uses classical logic to avoid assumption
`[DecidablePred P]`. See `Int.leastOfBdd` for a constructive counterpart.  -/
Int.exists_least_of_bdd : ∀ {P : ℤ → Prop}, (∃ b, ∀ (z : ℤ), P z → b ≤ z) → (∃ z, P z) → ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.inl_injective : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K),
  Function.Injective ⇑(LieAlgebra.SemiDirectSum.inl ψ)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_eq_getValueCastD_default : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
  [inst_2 : Inhabited (β a)], Std.Internal.List.getValueCast! a l = Std.Internal.List.getValueCastD a l default
-- Mathlib.Analysis.Meromorphic.Basic
/-- The composition of a meromorphic and an analytic function is meromorphic.  -/
MeromorphicAt.comp_analyticAt : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {F : Type u_5} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {x : 𝕜} {f : 𝕜' → F} {g : 𝕜 → 𝕜'},
  MeromorphicAt f (g x) → AnalyticAt 𝕜 g x → MeromorphicAt (f ∘ g) x