mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalAlgebra.elemental.instNonUnitalCommRingSubtypeMemNonUnitalSubalgebraOfT2Space : {R : Type u_3} →
  {A : Type u_4} →
    [inst : CommRing R] →
      [inst_1 : NonUnitalRing A] →
        [inst_2 : Module R A] →
          [inst_3 : IsScalarTower R A A] →
            [inst_4 : SMulCommClass R A A] →
              [inst_5 : TopologicalSpace A] →
                [inst_6 : IsSemitopologicalRing A] →
                  [inst_7 : ContinuousConstSMul R A] →
                    [T2Space A] → {x : A} → NonUnitalCommRing ↥(NonUnitalAlgebra.elemental R x)
-- Mathlib.Data.Finsupp.Option
Finsupp.some_single_none : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (m : M), (fun₀ | none => m).some = 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_eq_some_iff_exists_beq_and_mem_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {v : β},
  Std.DHashMap.Const.get? m k = some v ↔ ∃ k', (k == k') = true ∧ (k', v) ∈ Std.DHashMap.Const.toArray m
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.add : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x₁ x₂ y₁ y₂ : M}, x₁ ≡ y₁ [SMOD U] → x₂ ≡ y₂ [SMOD U] → x₁ + x₂ ≡ y₁ + y₂ [SMOD U]
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
/-- `-2` is a square in `F` iff `#F` is not congruent to `5` or `7` mod `8`.  -/
FiniteField.isSquare_neg_two_iff : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F], IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.of_symm_add : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : SMul R V] [inst_2 : AddCommMonoid V]
  (x y : HahnModule Γ R V), (HahnModule.of R).symm (x + y) = (HahnModule.of R).symm x + (HahnModule.of R).symm y
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.decodeSum.match_1.eq_2 : ∀ (motive : Bool → ℕ → Sort u_1) (x : Bool) (m : ℕ) (h_1 : (m : ℕ) → motive false m)
  (h_2 : (x : Bool) → (m : ℕ) → motive x m),
  (x = false → False) →
    (match x, m with
      | false, m => h_1 m
      | x, m => h_2 x m) =
      h_2 x m
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.map_dblZ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S)
  (P : Fin 3 → R), (W'.map f).dblZ (⇑f ∘ P) = f (W'.dblZ P)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.ext : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  {E F : Topology.RelCWComplex.Subcomplex C}, (∀ (x : X), x ∈ E ↔ x ∈ F) → E = F
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.IterM.step_intermediateZip.match_1.eq_1 : ∀ {α₁ β₁ : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β₁] {it₁ : Std.IterM m β₁}
  (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m β₁) (out : β₁)
  (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out))
  (h_1 :
    (it₁' : Std.IterM m β₁) →
      (out : β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, hp⟩)
  (h_2 :
    (it₁' : Std.IterM m β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩)
  (h_3 : (hp : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩),
  (match ⟨Std.IterStep.yield it₁' out, hp⟩ with
    | ⟨Std.IterStep.yield it₁' out, hp⟩ => h_1 it₁' out hp
    | ⟨Std.IterStep.skip it₁', hp⟩ => h_2 it₁' hp
    | ⟨Std.IterStep.done, hp⟩ => h_3 hp) =
    h_1 it₁' out hp
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.instInfSet.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  Subgroup.instInfSet =
    {
      sInf := fun s =>
        let __src := (⨅ S ∈ s, S.toSubmonoid).copy (⋂ S ∈ s, ↑S) ⋯;
        { toSubmonoid := __src, inv_mem' := ⋯ } }
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_ext₂_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {X Y Z : C} {f : J → C}
  {g h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y (⨁ f)) ⟶ Z},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.ι f j)))
          g =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.ι f j)))
          h) →
    g = h
-- Mathlib.CategoryTheory.Galois.Examples
/-- Given `f : X ⟶ Y` for `X Y : Action FintypeCat G`, the complement of the image
of `f` has a natural `G`-action.  -/
CategoryTheory.FintypeCat.Action.imageComplement : (G : Type u) → [inst : Group G] → {X Y : Action FintypeCat G} → (X ⟶ Y) → Action FintypeCat G
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The line between two points, as an affine subspace.  -/
«termLine[_,_,_]» : Lean.ParserDescr
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.powerRevlex_k : ℕ → ℕ → Ordering
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.source_inter_preimage_target_inter : ∀ {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) (s : Set (B × F)),
  e.source ∩ ↑e ⁻¹' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' s
-- Mathlib.CategoryTheory.Triangulated.Orthogonal
CategoryTheory.ObjectProperty.rightOrthogonal.map_bijective_of_isTriangulated : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [P.IsTriangulated] [CategoryTheory.IsTriangulated C] {Y : C},
  P.rightOrthogonal Y → ∀ (L : CategoryTheory.Functor C D) [L.IsLocalization P.trW] (X : C), Function.Bijective L.map
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.vecMul_cons : ∀ {α : Type u} {n : ℕ} {o' : Type uₒ} [inst : NonUnitalNonAssocSemiring α] (v : Fin n.succ → α) (w : o' → α)
  (B : Fin n → o' → α),
  Matrix.vecMul v (Matrix.of (Matrix.vecCons w B)) =
    Matrix.vecHead v • w + Matrix.vecMul (Matrix.vecTail v) (Matrix.of B)
-- Mathlib.RingTheory.LocalProperties.Submodule
/-- Let `N₁ N₂ : Submodule R M`. If the localization of `N₁` at each maximal ideal `P` is equal to
the localization of `N₂` at `P`, then `N₁ = N₂`.  -/
Submodule.eq_of_localization₀_maximal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5) [inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_4 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_5 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_5 : ∀ (P : Ideal R) [inst_5 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] {N₁ N₂ : Submodule R M},
  (∀ (P : Ideal R) [inst_6 : P.IsMaximal],
      Submodule.localized₀ P.primeCompl (f P) N₁ = Submodule.localized₀ P.primeCompl (f P) N₂) →
    N₁ = N₂
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
/-- A generalization of `HetT.bind` that provides the postcondition property to the mapping function.
 -/
Std.Iterators.HetT.pbind : {m : Type w → Type w'} →
  [Monad m] →
    {α : Type u} →
      {β : Type v} →
        (x : Std.Iterators.HetT m α) → ((a : α) → x.Property a → Std.Iterators.HetT m β) → Std.Iterators.HetT m β
-- Lean.Meta.NatTable
/-- Builds an expression of type `Nat → $type` that returns the `es[i]`, using binary search.
The array must be non-empty.
 -/
Lean.mkNatLookupTable : Lean.Expr → Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldr_reverse : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] N →ₗ[R] N)
  (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N) (x : CliffordAlgebra Q),
  ((CliffordAlgebra.foldr Q f hf) n) (CliffordAlgebra.reverse x) = ((CliffordAlgebra.foldl Q f hf) n) x
-- Mathlib.Topology.IsLocalHomeomorph
/-- A bijective local homeomorphism is a homeomorphism.  -/
IsLocalHomeomorph.toHomeomorphOfBijective : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f : X → Y} → IsLocalHomeomorph f → Function.Bijective f → X ≃ₜ Y
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.naturality_φ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp S₁.φ₂ f.f₂.τ₂ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.SnakeInput.functorP.map f) S₂.φ₂
-- Mathlib.Lean.Meta.CongrTheorems
Lean.Meta.FastSubsingleton.mk : ∀ {α : Sort u} [inst : Subsingleton α], Lean.Meta.FastSubsingleton α
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.mk.sizeOf_spec : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} [inst_11 : SizeOf 𝕜] [inst_12 : SizeOf E]
  [inst_13 : SizeOf F] [inst_14 : SizeOf H₁] [inst_15 : SizeOf H₂] [inst_16 : SizeOf M] [inst_17 : SizeOf N]
  (toPartialEquiv : PartialEquiv M N) (open_source : IsOpen toPartialEquiv.source)
  (open_target : IsOpen toPartialEquiv.target)
  (contMDiffOn_toFun : ContMDiffOn I J n (↑toPartialEquiv) toPartialEquiv.source)
  (contMDiffOn_invFun : ContMDiffOn J I n toPartialEquiv.invFun toPartialEquiv.target),
  sizeOf
      { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
        contMDiffOn_toFun := contMDiffOn_toFun, contMDiffOn_invFun := contMDiffOn_invFun } =
    1 + sizeOf toPartialEquiv + sizeOf open_source + sizeOf open_target
-- Std.Http.Data.Body.Empty
Std.Http.Body.instBEqEmpty.beq : Std.Http.Body.Empty → Std.Http.Body.Empty → Bool
-- Mathlib.Analysis.Calculus.MeanValue
/-- Let `s` be a convex set in a real normed vector space `E`, let `f : E → G` be a function
differentiable within `s` in a neighborhood of `x : E` with derivative `f'`. Suppose that `f'` is
continuous within `s` at `x`. Then for any number `K : ℝ≥0` larger than `‖f' x‖₊`, `f` is
`K`-Lipschitz on some neighborhood of `x` within `s`. See also
`Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt` for a version that claims
existence of `K` instead of an explicit estimate.  -/
Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {x : E} {f' : E → E →L[𝕜] G},
  Convex ℝ s →
    ∀ {f : E → G},
      (∀ᶠ (y : E) in nhdsWithin x s, HasFDerivWithinAt f (f' y) s y) →
        ContinuousWithinAt f' s x → ∀ (K : NNReal), ‖f' x‖₊ < K → ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.decidableMemZMultiples.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {a : G},
  AddSubgroup.decidableMemZMultiples = Classical.decPred fun x => x ∈ AddSubgroup.zmultiples a
-- Init.Data.Vector.Lemmas
Vector.instDecidableMemOfLawfulBEq : {α : Type u_1} → {n : ℕ} → [inst : BEq α] → [LawfulBEq α] → (a : α) → (as : Vector α n) → Decidable (a ∈ as)
-- Mathlib.Algebra.MvPolynomial.Derivation
MvPolynomial.mkDerivationₗ_monomial : ∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (MvPolynomial σ R) A] (f : σ → A) (s : σ →₀ ℕ) (r : R),
  (MvPolynomial.mkDerivationₗ R f) ((MvPolynomial.monomial s) r) =
    r • s.sum fun i k => (MvPolynomial.monomial (s - fun₀ | i => 1)) ↑k • f i
-- Mathlib.LinearAlgebra.BilinearForm.Hom
/-- Apply a linear map on the left and right argument of a bilinear form.  -/
LinearMap.BilinForm.comp : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {M' : Type w} →
            [inst_3 : AddCommMonoid M'] →
              [inst_4 : Module R M'] → LinearMap.BilinForm R M' → (M →ₗ[R] M') → (M →ₗ[R] M') → LinearMap.BilinForm R M
-- Std.Http.Data.Version
/-- `HTTP/1.0`
 -/
Std.Http.Version.v10 : Std.Http.Version
-- Mathlib.RingTheory.MvPolynomial.Basic
/-- The submodule of polynomials such that the degree with respect to each individual variable is
less than or equal to `m`.  -/
MvPolynomial.restrictDegree : (σ : Type u) → (R : Type v) → [inst : CommSemiring R] → ℕ → Submodule R (MvPolynomial σ R)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.inter_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp}, t₁.inter t₂ = t₁ ∩ t₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.getKey? k = (t.getKey? k).pfilter fun x h' => f x (t.get x ⋯)
-- Mathlib.Algebra.Lie.Submodule
/-- Given a Lie submodule `N` of a Lie module `M` over a Lie algebra `L`, and a Lie subalgebra
`H ≤ L`, `N.restr H` is the same submodule but viewed as a Lie submodule over `H`.  -/
LieSubmodule.restr : {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] →
                [inst_5 : LieAlgebra R L] → LieSubmodule R L M → (H : LieSubalgebra R L) → LieSubmodule R (↥H) M
-- Mathlib.RingTheory.Smooth.AdicCompletion
_private.Mathlib.RingTheory.Smooth.AdicCompletion.0.Algebra.FormallySmooth.liftAdicCompletionAux.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((m : ℕ) → motive m.succ.succ) → motive x
-- Mathlib.Probability.Moments.ComplexMGF
ProbabilityTheory.complexMGF_ofReal : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (x : ℝ),
  ProbabilityTheory.complexMGF X μ ↑x = ↑(ProbabilityTheory.mgf X μ x)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.instTransIsThetaTVSIsLittleOTVS : {α : Type u_1} →
  {𝕜 : Type u_3} →
    {E : Type u_4} →
      {F : Type u_5} →
        {G : Type u_6} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : AddCommGroup E] →
              [inst_2 : TopologicalSpace E] →
                [inst_3 : Module 𝕜 E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : TopologicalSpace F] →
                      [inst_6 : Module 𝕜 F] →
                        [inst_7 : AddCommGroup G] →
                          [inst_8 : TopologicalSpace G] →
                            [inst_9 : Module 𝕜 G] →
                              {l : Filter α} →
                                Trans (Asymptotics.IsThetaTVS 𝕜 l) (Asymptotics.IsLittleOTVS 𝕜 l)
                                  (Asymptotics.IsLittleOTVS 𝕜 l)
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.Nonempty.csInf_mem : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Finset α}, s.Nonempty → sInf ↑s ∈ s
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionOptions.toWorkDoneProgressOptions : Lean.Lsp.CodeActionOptions → Lean.Lsp.WorkDoneProgressOptions
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.withConstantsStructure : (L : FirstOrder.Language) →
  {M : Type w} →
    [L.Structure M] →
      (α : Type u_1) → [(FirstOrder.Language.constantsOn α).Structure M] → (L.withConstants α).Structure M
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- Let `p` be the minimal polynomial of an integral element `x`. If `p y` = 0, then `y` is a
conjugate root of `x`.
 -/
isConjRoot_of_aeval_eq_zero : ∀ {K : Type u_2} {A : Type u_5} [inst : Ring A] [inst_1 : Field K] [inst_2 : Algebra K A] [IsDomain A] {x y : A},
  IsIntegral K x → (Polynomial.aeval y) (minpoly K x) = 0 → IsConjRoot K x y
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.adj_congr_of_sym2 : ∀ {V : Type u} (G : SimpleGraph V) {u v w x : V}, s(u, v) = s(w, x) → (G.Adj u v ↔ G.Adj w x)
-- Aesop.Index.Basic
Aesop.IndexMatchResult.instToMessageData : {α : Type} → [Lean.ToMessageData α] → Lean.ToMessageData (Aesop.IndexMatchResult α)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.orderMonoidIso_symm : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedCommGroupWithZero Γ₀]
  [inst_1 : LinearOrderedCommGroupWithZero Γ'₀] [inst_2 : Ring R] {v : Valuation R Γ₀} {w : Valuation R Γ'₀}
  (h : v.IsEquiv w) (h' : w.IsEquiv v), h.orderMonoidIso.symm = h'.orderMonoidIso
-- Mathlib.Order.BoundedOrder.Monotone
monotone_and : ∀ {α : Type u} [inst : Preorder α] {p q : α → Prop}, Monotone p → Monotone q → Monotone fun x => p x ∧ q x
-- Mathlib.Combinatorics.SimpleGraph.LineGraph
SimpleGraph.IsIndContained.lineGraph : ∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'},
  G.IsIndContained G' → G.lineGraph.IsIndContained G'.lineGraph
-- Lean.Compiler.IR.CompilerM
Lean.IR.LogEntry.message.injEq : ∀ (msg msg_1 : Std.Format), (Lean.IR.LogEntry.message msg = Lean.IR.LogEntry.message msg_1) = (msg = msg_1)
-- Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
/-- Second part of the First Main Theorem of Value Distribution Theory, qualitative version: If `f` is
meromorphic on the complex plane, then the characteristic functions for the value `⊤` of the
function `f` and `f - a₀` agree asymptotically up to a bounded function.
 -/
ValueDistribution.isBigO_characteristic_sub_characteristic_shift : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a₀ : E} {f : ℂ → E},
  Meromorphic f →
    (ValueDistribution.characteristic f ⊤ - ValueDistribution.characteristic (fun x => f x - a₀) ⊤) =O[Filter.atTop] 1
-- Mathlib.Topology.Constructions
instLocallyCompactSpaceAdditive : ∀ {X : Type u} [inst : TopologicalSpace X] [LocallyCompactSpace X], LocallyCompactSpace (Additive X)
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.top_subtype_lowerCentralSeries : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (n : ℕ),
  AddSubgroup.map H.subtype (⊤.lowerCentralSeries n) = H.lowerCentralSeries n
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- A function which can be locally uniformly approximated by functions which are continuous at
a point is continuous at this point.  -/
continuousAt_of_locally_uniform_approx_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {f : α → β} {x : α},
  (∀ u ∈ uniformity β, ∃ t ∈ nhds x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u) → ContinuousAt f x
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.Raw.get? : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.LawfulEqCmp cmp] → Std.DTreeMap.Raw α β cmp → (a : α) → Option (β a)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_zero : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] [inst_2 : OrderTopology R]
  [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R] [inst_6 : SecondCountableTopology R]
  [inst_7 : DenselyOrdered R], StieltjesFunction.measure 0 = 0
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- Completeness of the uniform structure on `MvPowerSeries`  -/
MvPowerSeries.WithPiTopology.instCompleteSpace : ∀ {σ : Type u_1} {R : Type u_2} [inst : UniformSpace R] [CompleteSpace R], CompleteSpace (MvPowerSeries σ R)
-- Mathlib.CategoryTheory.Core
/-- The core of the identity functor is the identity functor on the cores.  -/
CategoryTheory.Functor.coreId : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (CategoryTheory.Functor.id C).core ≅ CategoryTheory.Functor.id (CategoryTheory.Core C)
-- Init.Data.Array.Lemmas
Array.set_append_right : ∀ {α : Type u_1} {xs ys : Array α} {i : ℕ} {x : α} (h' : i < (xs ++ ys).size) (h : xs.size ≤ i),
  (xs ++ ys).set i x h' = xs ++ ys.set (i - xs.size) x ⋯
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.iIndepFun.charFun_map_finsetSum_eq_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} {s : Finset ι} {E : Type u_3}
  [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : ι → Ω → E}
  [inst_4 : InnerProductSpace ℝ E],
  (∀ i ∈ s, AEMeasurable (X i) P) →
    ProbabilityTheory.iIndepFun (s.restrict X) P →
      MeasureTheory.charFun (MeasureTheory.Measure.map (∑ i ∈ s, X i) P) =
        ∏ i ∈ s, MeasureTheory.charFun (MeasureTheory.Measure.map (X i) P)
-- Mathlib.Data.Set.Finite.Basic
Set.finite_empty : ∀ {α : Type u}, ∅.Finite
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.setBernoulli_apply : ∀ {ι : Type u_1} {u : Set ι} {p : ↑unitInterval} (S : Set (Set ι)),
  (ProbabilityTheory.setBernoulli u p) S =
    (MeasureTheory.Measure.infinitePi fun i =>
        unitInterval.toNNReal p • MeasureTheory.Measure.dirac (i ∈ u) +
          unitInterval.toNNReal (unitInterval.symm p) • MeasureTheory.Measure.dirac False)
      ((fun t i => i ∈ t) '' S)
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.FixPoint.State.mk.inj : ∀ {usedFVarsMap : Lean.Elab.Term.MutualClosure.UsedFVarsMap} {modified : Bool}
  {usedFVarsMap_1 : Lean.Elab.Term.MutualClosure.UsedFVarsMap} {modified_1 : Bool},
  { usedFVarsMap := usedFVarsMap, modified := modified } = { usedFVarsMap := usedFVarsMap_1, modified := modified_1 } →
    usedFVarsMap = usedFVarsMap_1 ∧ modified = modified_1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.symmetry'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (P Q : C) {Z : C} (h : P ⨿ Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) h) =
    h
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivAt_add_const_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} (c : F), HasFDerivAt (fun x => f x + c) f' x ↔ HasFDerivAt f f' x