mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.closure_sdiff_sup_induction : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Set α},
  IsSublattice s →
    ⊥ ∈ s →
      ⊤ ∈ s →
        ∀ {p : (g : α) → g ∈ BooleanSubalgebra.closure s → Prop},
          (∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯) →
            (∀ (x : α) (hx : x ∈ BooleanSubalgebra.closure s) (y : α) (hy : y ∈ BooleanSubalgebra.closure s),
                p x hx → p y hy → p (x ⊔ y) ⋯) →
              ∀ (x : α) (hx : x ∈ BooleanSubalgebra.closure s), p x hx
-- Init.Data.Nat.MinMax
Nat.le_max_right : ∀ (a b : ℕ), b ≤ max a b
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.restrictScalars_symm_apply : ∀ (R : Type u_1) {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : TopologicalSpace M] [inst_6 : LinearMap.CompatibleSMul M M R S]
  (f : M ≃L[S] M) (a : M), (ContinuousLinearEquiv.restrictScalars R f).symm a = f.symm a
-- Mathlib.NumberTheory.ModularForms.Discriminant
/-- **Alias** of `ModularForm.tendsto_atImInfty_tprod_one_sub_eta_q_pow`. -/
ModularForm.discriminant_bounded_factor : Filter.Tendsto (fun x => ∏' (n : ℕ), (1 - ModularForm.eta_q n ↑x) ^ 24) UpperHalfPlane.atImInfty (nhds 1)
-- Mathlib.RingTheory.DedekindDomain.SInteger
/-- The `R`-subalgebra of `S`-integers of `K`.  -/
Set.integer : {R : Type u} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      Set (IsDedekindDomain.HeightOneSpectrum R) →
        (K : Type v) → [inst_2 : Field K] → [inst_3 : Algebra R K] → [IsFractionRing R K] → Subalgebra R K
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addX_of_X_eq' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → W'.addX P Q * (P 2 * Q 2) ^ 2 = (P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) ^ 2
-- Lean.Elab.Import
Lean.Elab.HeaderSyntax.isModule : Lean.Elab.HeaderSyntax → Bool
-- Mathlib.ModelTheory.Complexity
/-- An auxiliary operation to `FirstOrder.Language.BoundedFormula.toPrenex`.
If `φ` and `ψ` are in prenex normal form, then `φ.toPrenexImp ψ`
is a prenex normal form for `φ.imp ψ`.  -/
FirstOrder.Language.BoundedFormula.toPrenexImp : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → L.BoundedFormula α n → L.BoundedFormula α n
-- Lean.Meta.Basic
Lean.Meta.withCanUnfoldPred : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] → {α : Type} → (Lean.Meta.Config → Lean.ConstantInfo → Lean.CoreM Bool) → n α → n α
-- Lean.Setup
Lean.instCoeNameImport : Coe Lean.Name Lean.Import
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- The presheaf of smooth functions from `M` to `R`, for `R` a smooth commutative ring, as a
presheaf of commutative rings.  -/
smoothPresheafCommRing : {𝕜 : 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] →
              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] →
                                [ChartedSpace HM M] →
                                  (R : Type u) →
                                    [inst_9 : TopologicalSpace R] →
                                      [inst_10 : ChartedSpace H R] →
                                        [inst_11 : CommRing R] →
                                          [ContMDiffRing I (↑⊤) R] → TopCat.Presheaf CommRingCat (TopCat.of M)
-- Mathlib.Data.Finset.Sort
Finset.orderIsoOfFin_symm_apply : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) (x : ↥s),
  ↑((s.orderIsoOfFin h).symm x) = List.idxOf (↑x) (s.sort fun a b => a ≤ b)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
/-- The Weierstrass curve in affine coordinates base changed to an algebra `S` over `R`.  -/
WeierstrassCurve.Affine.baseChange : {R : Type r} →
  [inst : CommRing R] →
    WeierstrassCurve.Affine R → (S : Type s) → [inst_1 : CommRing S] → [Algebra R S] → WeierstrassCurve.Affine S
-- Mathlib.Data.Rat.Init
NNRatCast.mk : {K : Type u_1} → (ℚ≥0 → K) → NNRatCast K
-- Mathlib.Data.Seq.Computation
/-- `Promises s a`, or `s ~> a`, asserts that although the computation `s`
may not terminate, if it does, then the result is `a`.  -/
Computation.«term_~>_» : Lean.TrailingParserDescr
-- Mathlib.Order.Category.Preord
/-- Constructs an equivalence between preorders from an order isomorphism between them.  -/
Preord.Iso.mk : {α β : Preord} → ↑α ≃o ↑β → (α ≅ β)
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_eq_fintype_linearCombination : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Fintype α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (v : α → M),
  Finsupp.linearCombination R v ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R R α).symm = Fintype.linearCombination R v
-- Mathlib.Topology.Algebra.Group.Torsor
Homeomorph.smulConst_apply : ∀ {V : Type u_1} {P : Type u_2} [inst : Group V] [inst_1 : TopologicalSpace V] [inst_2 : Torsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalTorsor P] (p : P) (v : V), (Homeomorph.smulConst p) v = v • p
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.VAdd : {ι : Type u_1} → {M : Type u_2} → {α : ι → Type u_4} → [(i : ι) → VAdd M (α i)] → VAdd M ((i : ι) × α i)
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.liftOfSurjective_apply : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_1}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] {C : Type u_4} [inst_5 : CommRing C] [inst_6 : Algebra R C]
  [inst_7 : Algebra.FormallySmooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : Function.Surjective ⇑g)
  (hg' : IsNilpotent (RingHom.ker g)) (x : A), g ((Algebra.FormallySmooth.liftOfSurjective f g hg hg') x) = f x
-- Mathlib.Topology.Defs.Basic
/-- The complement of a closed set is an open set.  -/
IsClosed.isOpen_compl : ∀ {X : Type u} {inst : TopologicalSpace X} {s : Set X} [self : IsClosed s], IsOpen sᶜ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.isoBiprodZero_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (hY : CategoryTheory.Limits.IsZero Y),
  (CategoryTheory.Limits.isoBiprodZero hY).hom = CategoryTheory.Limits.biprod.inl
-- Mathlib.Data.Fin.Tuple.Basic
/-- Updating a nonzero element and taking the tail commute.  -/
Fin.tail_update_succ : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} (q : (i : Fin (n + 1)) → α i) (i : Fin n) (y : α i.succ),
  Fin.tail (Function.update q i.succ y) = Function.update (Fin.tail q) i y
-- Init.Data.List.ToArray
Array.replicate_eq_toArray_replicate : ∀ {n : ℕ} {α : Type u_1} {v : α}, Array.replicate n v = (List.replicate n v).toArray
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.diff_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₂.Equiv t₃ → (t₁ \ t₂).Equiv (t₁ \ t₃)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- One can reformulate being `Cⁿ` at a point as being `Cⁿ` in the source space when
composing with the extended chart.  -/
contMDiffAt_iff_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {n : WithTop ℕ∞},
  ContMDiffAt I I' n f x ↔
    ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I' n (f ∘ ↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) x)
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.le_of_matchesAt : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  pat ≠ "" → String.Slice.Pattern.Model.MatchesAt pat pos → pos.offset.increaseBy pat.utf8ByteSize ≤ s.rawEndPos
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
groupHomology.inhomogeneousChains.d.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (n : ℕ),
  groupHomology.inhomogeneousChains.d A n =
    ModuleCat.ofHom
      ((Finsupp.lsum k) fun g =>
        (Finsupp.lsingle fun i => g i.succ) ∘ₗ A.ρ (g 0)⁻¹ +
          ∑ j, (-1) ^ (↑j + 1) • Finsupp.lsingle (j.contractNth (fun x1 x2 => x1 * x2) g))
-- Mathlib.NumberTheory.Ostrowski
/-- The real-valued `AbsoluteValue` corresponding to the p-adic norm on `ℚ`.  -/
Rat.AbsoluteValue.padic : (p : ℕ) → [Fact (Nat.Prime p)] → AbsoluteValue ℚ ℝ
-- Mathlib.Topology.Category.Profinite.Projective
/-- For any profinite `X`, the natural map `Ultrafilter X → X` is a projective presentation.  -/
Profinite.projectivePresentation : (X : Profinite) → CategoryTheory.ProjectivePresentation X
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.isBigO_cocompact_zpow : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F) [ProperSpace E] (k : ℤ), ⇑f =O[Filter.cocompact E] fun x => ‖x‖ ^ k
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasFiniteColimits_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasFiniteLimits C],
  CategoryTheory.Limits.HasFiniteColimits Cᵒᵖ
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.rank_eq_one_of_flat_of_self_of_inj : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A : Subalgebra R S},
  A.LinearDisjoint A → ∀ [Module.Flat R ↥A], Function.Injective ⇑(algebraMap R S) → Module.rank R ↥A = 1
-- Mathlib.Geometry.Euclidean.Volume.Measure
MeasureTheory.isAddHaarMeasure_euclideanHausdorffMeasure : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E],
  (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)).IsAddHaarMeasure
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.comp_f₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃),
  (CategoryTheory.CategoryStruct.comp f g).f₀ = CategoryTheory.CategoryStruct.comp f.f₀ g.f₀
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
FiberBundle.writtenInExtChartAt_trivializationAt : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] {x : Bundle.TotalSpace F E}
  {y : EB × F},
  y ∈ (extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) x).target →
    writtenInExtChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F)) x
        (↑(trivializationAt F E x.proj)) y =
      y
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mul_left_coe_nonZeroDivisors_eq_zero_iff : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀] {x : M₀} {c : ↥(nonZeroDivisors M₀)}, ↑c * x = 0 ↔ x = 0
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.toMonoidHom_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β], Function.Injective OrderMonoidHom.toMonoidHom
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.left_unitor_inv_hom : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b), CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Data.ENNReal.Action
ENNReal.instIsOrderedSMulNNReal : IsOrderedSMul NNReal ENNReal
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instDistribMulActionForallOfMulAction : {M : Type u_1} →
  {α : Type u_3} →
    {A : Type u_5} → [inst : Monoid M] → [MulAction M α] → [inst_2 : AddMonoid A] → DistribMulAction Mᵈᵐᵃ (α → A)
-- Aesop.Exception
Aesop.commandDeclare_aesop_exception___ : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.smul_apply : ∀ {S : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : Module S V]
  [inst_6 : ContinuousConstSMul S V] [inst_7 : AddCommMonoid W] [inst_8 : Module R W] [inst_9 : TopologicalSpace W]
  [inst_10 : Module S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : SMulCommClass R S W] [inst_13 : SMul S R]
  [inst_14 : IsScalarTower S R V] [inst_15 : IsScalarTower S R W] (α : Sˣ) (e : V ≃L[R] W) (x : V), (α • e) x = ↑α • e x
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
/-- Converts a Lean `IntModule` expression `e` into a `LinExpr`

If `skipVar` is `true`, then the result is `none` if `e` is not an interpreted `IntModule` term.
We use `skipVar := false` when processing inequalities, and `skipVar := true` for equalities and disequalities
 -/
Lean.Meta.Grind.Arith.Linear.reify? : Lean.Expr → Bool → optParam ℕ 0 → Lean.Meta.Grind.Arith.Linear.LinearM (Option Lean.Meta.Grind.Arith.Linear.LinExpr)
-- Mathlib.Analysis.Analytic.Order
/-- The order of vanishing of `f` at `z₀`, as an element of `ℕ∞`.

The order is defined to be `∞` if `f` is identically 0 on a neighbourhood of `z₀`, and otherwise the
unique `n` such that `f` can locally be written as `f z = (z - z₀) ^ n • g z`, where `g` is analytic
and does not vanish at `z₀`. See `AnalyticAt.analyticOrderAt_eq_top` and
`AnalyticAt.analyticOrderAt_eq_natCast` for these equivalences.

If `f` isn't analytic at `z₀`, then `analyticOrderAt f z₀` returns a junk value of `0`.  -/
analyticOrderAt : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → 𝕜 → ℕ∞
-- Batteries.Data.UnionFind.Basic
/-- ### Union-find data structure

The `UnionFind` structure is an implementation of disjoint-set data structure
that uses path compression to make the primary operations run in amortized
nearly linear time. The nodes of a `UnionFind` structure `s` are natural
numbers smaller than `s.size`. The structure associates with a canonical
representative from its equivalence class. The structure can be extended
using the `push` operation and equivalence classes can be updated using the
`union` operation.

The main operations for `UnionFind` are:

* `empty`/`mkEmpty` are used to create a new empty structure.
* `size` returns the size of the data structure.
* `push` adds a new node to a structure, unlinked to any other node.
* `union` links two nodes of the data structure, joining their equivalence
  classes, and performs path compression.
* `find` returns the canonical representative of a node and updates the data
  structure using path compression.
* `root` returns the canonical representative of a node without altering the
  data structure.
* `checkEquiv` checks whether two nodes have the same canonical representative
  and updates the structure using path compression.

Most use cases should prefer `find` over `root` to benefit from the speedup from path-compression.

The main operations use `Fin s.size` to represent nodes of the union-find structure.
Some alternatives are provided:

* `unionN`, `findN`, `rootN`, `checkEquivN` use `Fin n` with a proof that `n = s.size`.
* `union!`, `find!`, `root!`, `checkEquiv!` use `Nat` and panic when the indices are out of bounds.
* `findD`, `rootD`, `checkEquivD` use `Nat` and treat out of bound indices as isolated nodes.

The noncomputable relation `UnionFind.Equiv` is provided to use the equivalence relation from a
`UnionFind` structure in the context of proofs.
 -/
Batteries.UnionFind : Type
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.mkPatternFromType.go : List Lean.Name → Lean.Expr → ℕ → ℕ → Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Meta.Sym.Pattern
-- Mathlib.Data.Complex.Basic
Complex.re_ofReal_mul : ∀ (r : ℝ) (z : ℂ), (↑r * z).re = r * z.re
-- Mathlib.NumberTheory.NumberField.CMField
/-- The index of the subgroup of `(𝓞 K)ˣ` generated by the real units and the roots of unity. This
index is equal to `1` or `2`, see `indexRealUnits_eq_one_or_two` and `indexRealUnits_eq_two_iff`.
 -/
NumberField.IsCMField.indexRealUnits : (K : Type u_1) → [Field K] → ℕ
-- Aesop.Tree.Data
Aesop.Rapp : Type
-- Aesop.RuleTac.Basic
Aesop.RuleApplication.postState : Aesop.RuleApplication → Lean.Meta.SavedState
-- Mathlib.Analysis.LocallyConvex.Separation
RCLike.separate_convex_open_set : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  {s : Set E},
  0 ∈ s → Convex ℝ s → IsOpen s → ∀ {x₀ : E}, x₀ ∉ s → ∃ f, RCLike.re (f x₀) = 1 ∧ ∀ x ∈ s, RCLike.re (f x) < 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) g'] {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackLeftPullbackSndIso f g g').hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst f (CategoryTheory.CategoryStruct.comp g' g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f g) g')
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h)
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_X : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.X.mirror = Polynomial.X
-- Lean.Meta.Sym.SymM
/-- Returns `true` if `sym.debug` is set  -/
Lean.Meta.Sym.isDebugEnabled : Lean.Meta.Sym.SymM Bool
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.keys_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.keys = t₂.keys
-- Init.Data.String.Iterator
/-- Moves the iterator forward until the Boolean predicate `p` returns `true` for the iterator's current
character or until the end of the string is reached. Does nothing if the current character already
satisfies `p`.
 -/
String.Legacy.Iterator.find : String.Legacy.Iterator → (Char → Bool) → String.Legacy.Iterator
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instNonUnitalNormedRing : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    [CompactSpace α] → {R : Type u_4} → [inst_2 : NonUnitalNormedRing R] → NonUnitalNormedRing C(α, R)
-- Lean.Meta.DiscrTree.Basic
/-- Helper function for converting an entry (i.e., `Array Key`) to the discrimination tree into
`MessageData` that is more user-friendly. We use this function to implement diagnostic information.
 -/
Lean.Meta.DiscrTree.keysAsPattern : Array Lean.Meta.DiscrTree.Key → Lean.CoreM Lean.MessageData
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M), ↑↑N = ↑N
-- Mathlib.Data.Set.Card
Set.encard_union_eq : ∀ {α : Type u_1} {s t : Set α}, Disjoint s t → (s ∪ t).encard = s.encard + t.encard
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {l : List α}
  {k fallback : α}, k ∈ t → (t.insertMany l).getD k fallback = t.getD k fallback
-- Mathlib.Combinatorics.Hindman
Hindman.FS.below : {M : Type u_1} →
  [inst : AddSemigroup M] →
    {motive : (a : Stream' M) → (a_1 : M) → Hindman.FS a a_1 → Prop} →
      {a : Stream' M} → {a_1 : M} → Hindman.FS a a_1 → Prop
-- Mathlib.Analysis.Normed.Group.Indicator
enorm_indicator_le_enorm_self : ∀ {α : Type u_1} {ε : Type u_2} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] {s : Set α} (f : α → ε)
  (a : α), ‖s.indicator f a‖ₑ ≤ ‖f a‖ₑ
-- Mathlib.Analysis.Normed.Field.Krasner
/-- Given a field extension `L / K` where `L` is a normed field, `IsKrasner K L` is the abstraction
of the conclusion of Krasner's lemma. That is, `IsKrasner K L` means that given two elements
`x y : L`, such that `x` is separable over `K`, all conjugate roots of `x` live in `L`,
`y` is integral over `K`, and the distance between `x` and `y` is less than the distance between
`x` and any other conjugate root of `x`, then `x` is in the field generated by `K` and `y`.
 -/
IsKrasner : (K : Type u_1) → (L : Type u_2) → [inst : NormedField L] → [inst_1 : Field K] → [Algebra K L] → Prop
-- Mathlib.Order.Comparable
instTransIncompRelLeAntisymmRel : {α : Type u_1} →
  [inst : Preorder α] →
    Trans (IncompRel fun x1 x2 => x1 ≤ x2) (AntisymmRel fun x1 x2 => x1 ≤ x2) (IncompRel fun x1 x2 => x1 ≤ x2)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- The functoriality of the intermediate object in the
factorization of the small object argument.  -/
CategoryTheory.SmallObject.objMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [inst_3 : I.IsCardinalForSmallObjectArgument κ] →
              {f g : CategoryTheory.Arrow C} →
                (f ⟶ g) → (CategoryTheory.SmallObject.obj I κ f.hom ⟶ CategoryTheory.SmallObject.obj I κ g.hom)
-- Mathlib.Order.SymmDiff
Bool.symmDiff_eq_xor : ∀ (p q : Bool), symmDiff p q = (p ^^ q)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.one_le_ceil_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}, 1 ≤ ⌈a⌉₊ ↔ 0 < a
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothPresheafGroup.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (G : Type u)
  [inst_9 : TopologicalSpace G] [inst_10 : ChartedSpace H G] [inst_11 : Group G] [inst_12 : LieGroup I (↑⊤) G],
  smoothPresheafGroup IM I M G =
    { obj := fun U => GrpCat.of ((smoothSheaf IM I M G).presheaf.obj U),
      map := fun {X Y} h => GrpCat.ofHom (ContMDiffMap.restrictMonoidHom IM I G ⋯), map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.ofAddUnits.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)),
  S.ofAddUnits = AddSubmonoid.map (AddUnits.coeHom M) S.toAddSubmonoid