mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Countable.Defs
Function.Surjective.countable : ∀ {α : Sort u} {β : Sort v} [Countable α] {f : α → β}, Function.Surjective f → Countable β
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.support_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R], HahnSeries.support 0 = ∅
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.evalEval_polynomialX : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} (x y : R),
  Polynomial.evalEval x y W.polynomialX = W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.SignedMeasure.toMeasureOfLEZero.congr_simp : ∀ {α : Type u_1} {m : MeasurableSpace α} (s s_1 : MeasureTheory.SignedMeasure α) (e_s : s = s_1) (i i_1 : Set α)
  (e_i : i = i_1) (hi₁ : MeasurableSet i)
  (hi₂ : MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i),
  s.toMeasureOfLEZero i hi₁ hi₂ = s_1.toMeasureOfLEZero i_1 ⋯ ⋯
-- Mathlib.RingTheory.Localization.AtPrime.Extension
IsLocalization.AtPrime.equivQuotientMapMaximalIdeal_apply_mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Rₚ : Type u_3) [inst_4 : CommRing Rₚ] [inst_5 : Algebra R Rₚ]
  [inst_6 : IsLocalization.AtPrime Rₚ p] [inst_7 : IsLocalRing Rₚ] (Sₚ : Type u_4) [inst_8 : CommRing Sₚ]
  [inst_9 : Algebra S Sₚ] [inst_10 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
  [inst_11 : Algebra Rₚ Sₚ] [inst_12 : Algebra R Sₚ] [inst_13 : IsScalarTower R S Sₚ] [inst_14 : IsScalarTower R Rₚ Sₚ]
  [inst_15 : p.IsMaximal] (x : S),
  (IsLocalization.AtPrime.equivQuotientMapMaximalIdeal S p Rₚ Sₚ)
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap Rₚ Sₚ) (IsLocalRing.maximalIdeal Rₚ))) ((algebraMap S Sₚ) x)
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous₂.eq_1 : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  (f : α → β → γ), UniformContinuous₂ f = UniformContinuous (Function.uncurry f)
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projection_apply_right`. -/
Submodule.IsCompl.projection_apply_right : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) (x : ↥q), (p.projection q h) ↑x = 0
-- Mathlib.Order.Defs.LinearOrder
eq_min : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, c ≤ a → c ≤ b → (∀ {d : α}, d ≤ a → d ≤ b → d ≤ c) → c = min a b
-- Init.Data.BitVec.Basic
/-- Notation for bitvector literals. `i#n` is a shorthand for `BitVec.ofNat n i`. 

Conventions for notations in identifiers:

 * The recommended spelling of `0#n` in identifiers is `zero` (not `ofNat_zero`).

 * The recommended spelling of `1#n` in identifiers is `one` (not `ofNat_one`). -/
BitVec.«term__#__» : Lean.ParserDescr
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.swap.eq_1 : ∀ (M : Type u_1) (N : Type u_2) [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Monoid.Coprod.swap M N = Monoid.Coprod.clift (Monoid.Coprod.mk.comp (FreeMonoid.map Sum.swap)) ⋯ ⋯ ⋯ ⋯
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.expandIfNecessary.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DHashMap.Internal.Raw₀ α β → Sort u_3) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size)
  (h_1 :
    (size : ℕ) →
      (buckets : Array (Std.DHashMap.Internal.AssocList α β)) →
        (hm : 0 < { size := size, buckets := buckets }.buckets.size) →
          motive ⟨{ size := size, buckets := buckets }, hm⟩),
  (match ⟨{ size := size, buckets := buckets }, hm⟩ with
    | ⟨{ size := size, buckets := buckets }, hm⟩ => h_1 size buckets hm) =
    h_1 size buckets hm
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_of_isEmpty : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)] [IsEmpty ι]
  (w : ι → ℝ) (f g : (i : ι) → E i), ⟪f, g⟫_[𝕜, w] = 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Measurable.dist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : MeasurableSpace β] [SecondCountableTopology α] {f g : β → α},
  Measurable f → Measurable g → Measurable fun b => dist (f b) (g b)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_star : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {R : Type u_5} [inst_1 : TopologicalSpace R]
  [inst_2 : Star R] [inst_3 : ContinuousStar R] (f : α →ₘ[μ] R), ↑(star f) =ᵐ[μ] star ↑f
-- Init.Data.String.Iterate
/-- Creates an iterator over all characters \(Unicode code points\) in `s`.

Examples:

* `"abc".toSlice.chars.toList = ['a', 'b', 'c']`

* `"ab∀c".toSlice.chars.toList = ['a', 'b', '∀', 'c']`
 -/
String.Slice.chars : (s : String.Slice) → Std.Iter Char
-- Mathlib.Util.SynthesizeUsing
/-- `synthesizeUsing' type tacticSyntax` synthesizes an element of type `type` by evaluating the
given tactic syntax.

Example:
```lean
let e ← synthesizeUsingTactic' ty (← `(tactic| norm_num))
```

The tactic must solve for all goals, in contrast to `synthesizeUsingTactic`.

If you need to insert expressions into a tactic proof, then you might use `synthesizeUsing'`
directly, since the `TacticM` monad has access to the `TermElabM` monad. For example, here
is a term elaborator that wraps the `simp at ...` tactic:
```
def simpTerm (e : Expr) : MetaM Expr := do
  let mvar ← Meta.mkFreshTypeMVar
  let e' ← synthesizeUsing' mvar
    (do evalTactic (← `(tactic| have h := $(← Term.exprToSyntax e); simp at h; exact h)))
  -- Note: `simp` does not always insert type hints, so to ensure that we get a term
  -- with the simplified type (as opposed to one that is merely defeq), we should add
  -- a type hint ourselves.
  Meta.mkExpectedTypeHint e' mvar

elab "simpTerm% " t:term : term => do simpTerm (← Term.elabTerm t none)
```
 -/
synthesizeUsingTactic' : {u : Lean.Level} → (type : Q(Sort u)) → Lean.Syntax → Lean.MetaM Q(«$type»)
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.int_sub_iff : ∀ {p x : ℝ} {m : ℤ}, LiouvilleWith p (↑m - x) ↔ LiouvilleWith p x
-- Aesop.Forward.PremiseIndex
Aesop.instLEPremiseIndex : LE Aesop.PremiseIndex
-- Mathlib.Order.Hom.Bounded
TopHom.instLattice : {α : Type u_2} → {β : Type u_3} → [inst : Top α] → [inst_1 : Lattice β] → [inst_2 : OrderTop β] → Lattice (TopHom α β)
-- Mathlib.Data.Part
/-- Extract a value from a partial value given a proof of `Dom`  -/
Part.get : {α : Type u} → (self : Part α) → self.Dom → α
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddCommMonoid.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : AddCommMonoid M],
  Filter.Germ.instAddCommMonoid = { toAddMonoid := Filter.Germ.instAddMonoid, add_comm := ⋯ }
-- Mathlib.Data.Nat.Factors
_private.Mathlib.Data.Nat.Factors.0.Nat.primeFactorsList.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((k : ℕ) → motive k.succ.succ) → motive x
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Type of normalized 1-morphisms `((... ≫ h) ≫ g) ≫ f`.  -/
Mathlib.Tactic.BicategoryLike.NormalizedHom : Type
-- Mathlib.RingTheory.Coalgebra.Convolution
/-- Convolution ring structure on linear maps from a coalgebra to an algebra.  -/
LinearMap.convRing : {R : Type u_1} →
  {A : Type u_3} →
    {C : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : Ring A] →
          [inst_2 : AddCommMonoid C] →
            [inst_3 : Algebra R A] → [inst_4 : Module R C] → [Coalgebra R C] → Ring (WithConv (C →ₗ[R] A))
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.isOrthogonal_reflection : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (self : RootPairing.RootPositiveForm S P) (i : ι), LinearMap.IsOrthogonal self.form ⇑(P.reflection i)
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `Irreducible (cyclotomic p K)` (in particular for `K = ℚ`) and `p` is an odd prime,
then the norm of `zeta p K L - 1` is `p`.  -/
IsCyclotomicExtension.norm_zeta_sub_one_of_prime_ne_two : ∀ {p : ℕ} {K : Type u} (L : Type v) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Fact (Nat.Prime p)] [inst_4 : IsCyclotomicExtension {p} K L],
  Irreducible (Polynomial.cyclotomic p K) → p ≠ 2 → (Algebra.norm K) (IsCyclotomicExtension.zeta p K L - 1) = ↑p
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_X_sub_C : ∀ {S : Type v} [inst : Ring S] (r : S), (Polynomial.X - Polynomial.C r).leadingCoeff = 1
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.spaceUptoLine : Std.Format → Bool → ℤ → ℕ → Std.Format.SpaceResult✝
-- Lean.Parser.Extension
/-- Resolve the given parser name and return a list of candidates.  -/
Lean.Parser.resolveParserName : Lean.Ident → Lean.CoreM (List Lean.Parser.ParserResolution)
-- Mathlib.Data.Set.Image
Set.range_eq_iff : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β), Set.range f = s ↔ (∀ (a : α), f a ∈ s) ∧ ∀ b ∈ s, ∃ a, f a = b
-- Init.Data.List.Sublist
List.subset_append_of_subset_right : ∀ {α : Type u_1} {l l₂ : List α} (l₁ : List α), l ⊆ l₂ → l ⊆ l₁ ++ l₂
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isBounded_iff_isVonNBounded : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousSMul 𝕜 E] {s : Set E},
  Bornology.IsBounded s ↔ Bornology.IsVonNBounded 𝕜 s
-- Mathlib.Data.Num.Lemmas
Num.bit1.eq_1 : Num.zero.bit1 = 1
-- Mathlib.Topology.Constructions
instTopologicalSpaceAdditive : {X : Type u} → [TopologicalSpace X] → TopologicalSpace (Additive X)
-- Mathlib.Order.Monotone.Defs
Subsingleton.strictAnti : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] [Subsingleton α] (f : α → β), StrictAnti f
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.natCast_add_one_le_iff : ∀ {n : ℕ} {c : Cardinal.{u_1}}, ↑n + 1 ≤ c ↔ ↑n < c
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.topologicalAddGroup : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F],
  IsTopologicalAddGroup (E →SL[σ] F)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.leadingCoeff_of_c_eq_zero' : ∀ {R : Type u_1} {d : R} [inst : Semiring R], { a := 0, b := 0, c := 0, d := d }.toPoly.leadingCoeff = d
-- Mathlib.Algebra.Ring.Equiv
/-- The identity map is a ring isomorphism.  -/
RingEquiv.refl : (R : Type u_4) → [inst : Mul R] → [inst_1 : Add R] → R ≃+* R
-- Init.Data.List.Count
List.count_nil : ∀ {α : Type u_1} [inst : BEq α] {a : α}, List.count a [] = 0
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int32.reduceOfInt : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.LocallyConvex.Separation
RCLike.geometric_hahn_banach_closed_point : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {s : Set E}
  {x : E} [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E],
  Convex ℝ s → IsClosed s → x ∉ s → ∃ f u, (∀ a ∈ s, RCLike.re (f a) < u) ∧ u < RCLike.re (f x)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.Away.isLocalizationElem.congr_simp : ∀ {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {e e_1 : ℕ} (e_e : e = e_1) {d d_1 : ℕ} (e_d : d = d_1) {f : A} (hf : f ∈ 𝒜 d) {g g_1 : A}
  (e_g : g = g_1) (hg : g ∈ 𝒜 e),
  HomogeneousLocalization.Away.isLocalizationElem hf hg = HomogeneousLocalization.Away.isLocalizationElem ⋯ ⋯
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.closure_withConstants_eq : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A s : Set M},
  (FirstOrder.Language.Substructure.closure (L.withConstants ↑A)).toFun s =
    ((FirstOrder.Language.Substructure.closure L).toFun (A ∪ s)).withConstants ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.isIso_snd_iso_of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y : C} {fst snd : P ⟶ X} {f : X ⟶ Y},
  CategoryTheory.IsPullback fst snd f f →
    autoParam (CategoryTheory.Mono f) CategoryTheory.IsPullback.isIso_snd_iso_of_mono._auto_1 → CategoryTheory.IsIso snd
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instReprCnstrRHS : Repr Lean.Meta.Grind.CnstrRHS
-- Init.Data.Zero
One.ofOfNat1 : {α : Type u_1} → [OfNat α 1] → One α
-- Mathlib.Data.EReal.Operations
EReal.coe_mul_top_of_pos : ∀ {x : ℝ}, 0 < x → ↑x * ⊤ = ⊤
-- Mathlib.Analysis.LocallyConvex.Bounded
NormedSpace.isVonNBounded_closedBall : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  (r : ℝ), Bornology.IsVonNBounded 𝕜 (Metric.closedBall 0 r)
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.Measure.sigmaFiniteSetGE.congr_simp : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ μ_1 : MeasureTheory.Measure α),
  μ = μ_1 →
    ∀ (ν ν_1 : MeasureTheory.Measure α) (e_ν : ν = ν_1) [inst : MeasureTheory.IsFiniteMeasure ν] (n n_1 : ℕ),
      n = n_1 → ∀ (a a_1 : α), a = a_1 → μ.sigmaFiniteSetGE ν n a = μ_1.sigmaFiniteSetGE ν_1 n_1 a_1
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_target : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H},
  (f.extend I).target = ↑I.symm ⁻¹' f.target ∩ Set.range ↑I
-- Mathlib.Algebra.Group.Hom.Basic
/-- If `G` is commutative and `G →* H` is surjective, then `H` is commutative.  -/
MonoidHom.commGroupOfSurjective : {G : Type u_5} →
  {H : Type u_6} → [inst : CommGroup G] → [inst_1 : Group H] → (f : G →* H) → Function.Surjective ⇑f → CommGroup H
-- Mathlib.Data.Set.Defs
/-- `{ f x y | (x : X) (y : Y) }` is notation for the set of elements `f x y` constructed from the
binders `x` and `y`, equivalent to `{z : Z | ∃ x y, f x y = z}`.

If `f x y` is a single identifier, it must be parenthesized to avoid ambiguity with `{x | p x}`;
for instance, `{(x) | (x : Nat) (y : Nat) (_hxy : x = y^2)}`.
 -/
Mathlib.Meta.«term{_|_}» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
/-- Pull a submonoid back to an opposite submonoid along `MulOpposite.unop`  -/
Submonoid.op : {M : Type u_2} → [inst : MulOneClass M] → Submonoid M → Submonoid Mᵐᵒᵖ
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- `exp (-a * x) = o(x ^ s)` as `x → ∞`, for any positive `a` and real `s`.  -/
isLittleO_exp_neg_mul_rpow_atTop : ∀ {a : ℝ}, 0 < a → ∀ (b : ℝ), (fun x => Real.exp (-a * x)) =o[Filter.atTop] fun x => x ^ b
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- If `v` is a real infinite place, then the embedding `v.Completion →+* ℝ` is surjective.  -/
NumberField.InfinitePlace.Completion.surjective_extensionEmbeddingOfIsReal : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} (hv : v.IsReal),
  Function.Surjective ⇑(NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hv)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.negPart_one : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A], 1⁻ = 0
-- Lean.Meta.CongrTheorems
Lean.Meta.instInhabitedCongrArgKind.default : Lean.Meta.CongrArgKind
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
IsStarNormal.instNonUnitalContinuousFunctionalCalculus : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A], NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℂ A IsStarNormal
-- Mathlib.Order.Partition.Finpartition
Finpartition.ofPairwiseDisjoint.eq_1 : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] (parts : Finset α)
  (hdisjoint : (↑parts).PairwiseDisjoint id),
  Finpartition.ofPairwiseDisjoint parts hdisjoint =
    { parts := parts.erase ⊥, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.limNthHom_zero : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1),
  PadicInt.limNthHom f_compat 0 = 0
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.instInhabitedStruct.default : Lean.Meta.Grind.Arith.Linear.Struct
-- Mathlib.Algebra.Group.Action.Basic
arrowAddAction.eq_1 : ∀ {G : Type u_7} {A : Type u_8} {B : Type u_9} [inst : SubtractionMonoid G] [inst_1 : AddAction G A],
  arrowAddAction = { vadd := fun g F a => F (-g +ᵥ a), add_vadd := ⋯, zero_vadd := ⋯ }
-- Init.Data.String.TakeDrop
/-- Returns the position at the start of the longest suffix of `s` for which `pat` matches
\(potentially repeatedly\).
 -/
String.skipSuffixWhile : {ρ : Type} → (s : String) → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → s.Pos
-- Mathlib.Analysis.Convex.Intrinsic
/-- The intrinsic interior of a set is its interior considered as a set in its affine span.  -/
intrinsicInterior : (𝕜 : Type u_1) →
  {V : Type u_2} →
    {P : Type u_5} →
      [inst : Ring 𝕜] →
        [inst_1 : AddCommGroup V] → [Module 𝕜 V] → [TopologicalSpace P] → [AddTorsor V P] → Set P → Set P
-- Mathlib.Data.List.ReduceOption
List.reduceOption_length_lt_iff : ∀ {α : Type u_1} {l : List (Option α)}, l.reduceOption.length < l.length ↔ none ∈ l
-- Mathlib.Data.Nat.Sqrt
Nat.le_sqrt' : ∀ {m n : ℕ}, m ≤ n.sqrt ↔ m ^ 2 ≤ n
-- Init.Data.Array.Basic
/-- Applies the monadic action `f` to every element in the array, along with the element's index and a
proof that the index is in bounds, from left to right. Returns the array of results.
 -/
Array.mapFinIdxM : {α : Type u} →
  {β : Type v} → {m : Type v → Type w} → [Monad m] → (as : Array α) → ((i : ℕ) → α → i < as.size → m β) → m (Array β)
-- Init.Data.String.Iterator
/-- Gets the character at the iterator's current position.

The proof of `it.hasNext` ensures that there is, in fact, a character at the current position. This
function is faster that `String.Iterator.curr` due to avoiding a run-time bounds check.
 -/
String.Legacy.Iterator.curr' : (it : String.Legacy.Iterator) → it.hasNext = true → Char
-- Init.Grind.Order
Lean.Grind.Order.le_of_eq_2_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b : α}, a = b → b ≤ a + ↑0
-- Std.Data.ExtDTreeMap.Basic
/-- Implementation detail of the tree map  -/
Std.ExtDTreeMap.lift₂ : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {γ : Sort w} →
        (f : Std.DTreeMap α β cmp → Std.DTreeMap α β cmp → γ) →
          (∀ (a b c d : Std.DTreeMap α β cmp), a.Equiv c → b.Equiv d → f a b = f c d) →
            Std.ExtDTreeMap α β cmp → Std.ExtDTreeMap α β cmp → γ
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj.eq_2 : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) (i j : ι),
  TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj U (CategoryTheory.Pairwise.pair i j) =
    { obj := U i ⊓ U j, property := ⋯ }
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.eq_of_natDegree_lt_card_of_eval_eq' : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] (p q : Polynomial R) (s : Finset R),
  (∀ i ∈ s, Polynomial.eval i p = Polynomial.eval i q) → max p.natDegree q.natDegree < s.card → p = q
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.coneEquiv_counitIso_inv_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)}
  (X_1 : CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K)),
  (CategoryTheory.WithTerminal.coneEquiv.counitIso.inv.app X_1).hom = CategoryTheory.CategoryStruct.id X_1.pt
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_filterMapM_map : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst_8 : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → γ} {g : γ → n (Option δ)} {it : Std.IterM m β},
  (Std.IterM.filterMapM g (Std.IterM.map f it)).toArray = (Std.IterM.filterMapM (fun b => g (f b)) it).toArray
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_eq_Ioc_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c d : α}, a < b ∨ c < d → (Set.Ioc a b = Set.Ioc c d ↔ a = c ∧ b = d)
-- Init.Data.Vector.Lemmas
Vector.toList_cast : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} (h : n = m), (Vector.cast h xs).toList = xs.toList
-- Mathlib.Data.Num.Bitwise
SNum.nz.injEq : ∀ (a a_1 : NzsNum), (SNum.nz a = SNum.nz a_1) = (a = a_1)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instDivisionMonoid.eq_1 : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : DivisionMonoid G],
  Filter.Germ.instDivisionMonoid =
    { toDivInvMonoid := Filter.Germ.instDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_iSup : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Add M] (S : ι → AddSubsemigroup M), (iSup S).op = ⨆ i, (S i).op
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.section_comp_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B)
  [inst_1 : CategoryTheory.IsReflexivePair f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.commonSection f g) g = CategoryTheory.CategoryStruct.id B
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.center_le_radical : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieAlgebra.center R L ≤ LieAlgebra.radical R L
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq_zero : ∀ {K : Type u_1} [inst : RCLike K], RCLike.normSq 0 = 0
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instIsSubApplyUpperHalfPlaneComplex : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ}, IsSubApply (ModularForm Γ k) UpperHalfPlane ℂ
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.PreOneHypercover.functorPushforward_sieve₁'_of_preservesLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} {E : CategoryTheory.PreOneHypercover X} (F : CategoryTheory.Functor C D) (i₁ i₂ : E.I₀)
  [inst_2 : CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (E.f i₁) (E.f i₂)) F],
  CategoryTheory.Sieve.functorPushforward F (E.sieve₁' i₁ i₂) =
    (E.map F).sieve₁ (F.map (CategoryTheory.Limits.pullback.fst (E.f i₁) (E.f i₂)))
      (F.map (CategoryTheory.Limits.pullback.snd (E.f i₁) (E.f i₂)))