mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_nonpos_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  (f : R → R) (a : A),
  autoParam (ContinuousOn f (spectrum R a)) cfc_nonpos_iff._auto_1 →
    autoParam (p a) cfc_nonpos_iff._auto_3 → (cfc f a ≤ 0 ↔ ∀ x ∈ spectrum R a, f x ≤ 0)
-- Plausible.Shrinkable
Plausible.Shrinkable.mk : {α : Type u} → (α → List α) → Plausible.Shrinkable α
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.sub_mem : ∀ {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 y : M}, x ≡ y [SMOD U] ↔ x - y ∈ U
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_unitIso_hom_app_app_snd : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (X_1 : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) (X_2 : X),
  (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).unitIso.hom.app X_1).app X_2).snd =
    CategoryTheory.CategoryStruct.id (X_1.obj X_2).snd
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.whisker_ι : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f)
  (g : K ≃ J) (k : K), (c.whisker g).ι k = c.ι (g k)
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fdiv_cancel_left : ∀ {a : ℤ} (b : ℤ), a ≠ 0 → (a * b).fdiv a = b
-- Mathlib.Algebra.Ring.BooleanRing
toBoolRing_bot : ∀ {α : Type u_1} [inst : BooleanAlgebra α], toBoolRing ⊥ = 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.async : Lean.Lsp.SemanticTokenModifier
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- `insert` preserves well-formedness. Later shown to be subsumed by `.wf`.  -/
Std.DTreeMap.Internal.Impl.WF.insert : ∀ {α : Type u} [inst : Ord α] {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k},
  t.WF → (Std.DTreeMap.Internal.Impl.insert k v t h).impl.WF
-- Init.Internal.Order.MonadTail
Lean.Order.instMonadTailExceptT : {ε : Type u} → {m : Type u → Type v} → [inst : Monad m] → [Lean.Order.MonadTail m] → Lean.Order.MonadTail (ExceptT ε m)
-- Mathlib.NumberTheory.PrimeCounting
/-- The prime counting function: Returns the number of primes less than or equal to the input.

With `open scoped Nat.Prime`, this has notation `π`.  -/
Nat.Prime.termπ : Lean.ParserDescr
-- Mathlib.Order.UpperLower.Relative
isRelUpperSet_Icc_le : ∀ {α : Type u_1} {a : α} [inst : Preorder α] {c : α}, IsRelUpperSet (Set.Icc a c) fun x => x ≤ c
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_neg : ∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] (x : R) (y : ↥M), IsLocalization.mk' S (-x) y = -IsLocalization.mk' S x y
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.mulLeft_eq_zero_iff : ∀ (R : Type u_6) (A : Type u_7) [inst : Semiring R] [inst_1 : NonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] (a : A), LinearMap.mulLeft R a = 0 ↔ a = 0
-- Batteries.Recycling.RBTree.Basic
RBTree.RBSet.instToStreamStream : {α : Type u_1} → {cmp : α → α → Ordering} → Std.ToStream (RBTree.RBSet α cmp) (RBTree.RBNode.Stream α)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal : ∀ {θ ψ : Real.Angle},
  θ.sign = ψ.sign → θ.sign ≠ (θ + ψ).sign → |(θ + ψ).toReal| = 2 * Real.pi - (|θ.toReal| + |ψ.toReal|)
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_le_length_mul_add_left : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w₁ w₂ : W),
  cs.length w₂ ≤ cs.length (w₁ * w₂) + cs.length w₁
-- Mathlib.Data.Vector.Basic
/-- Opposite direction of `Vector.pmap_cons`  -/
List.Vector.pmap_cons' : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f : (a : α) → p a → β) (a : α) (v : List.Vector α n) (ha : p a)
  (hp : ∀ x ∈ v.toList, p x), f a ha ::ᵥ List.Vector.pmap f v hp = List.Vector.pmap f (a ::ᵥ v) ⋯
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
/-- Returns the `GenContFract` of a value. In fact, the returned gcf is also a `ContFract` that
terminates if and only if `v` is rational
(see `Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean`).

The continued fraction representation of `v` is given by `[⌊v⌋; b₀, b₁, b₂,...]`, where
`[b₀; b₁, b₂,...]` recursively is the continued fraction representation of `1 / (v - ⌊v⌋)`. This
process stops when the fractional part `v - ⌊v⌋` hits 0 at some step.

The implementation uses `IntFractPair.stream` to obtain the partial denominators of the continued
fraction. Refer to said function for more details about the computation process.
 -/
GenContFract.of : {K : Type u_1} → [inst : DivisionRing K] → [inst_1 : LinearOrder K] → [FloorRing K] → K → GenContFract K
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.diam_eq_zero_of_not_connected : ∀ {α : Type u_1} {G : SimpleGraph α}, ¬G.Connected → G.diam = 0
-- Lean.Elab.DocString
/-- The syntax that the value was derived from.  -/
Lean.Doc.WithSyntax.stx : {α : Type u} → Lean.Doc.WithSyntax α → Lean.Syntax
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- A wide pullback cone is a cone on the wide cospan formed by a family of morphisms.  -/
CategoryTheory.Limits.WidePullbackCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} → {X : C} → {Y : ι → C} → ((i : ι) → Y i ⟶ X) → Type (max (max u_1 u) v)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.rightCont_eq_of_isMax : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : PartialOrder ι] (𝓕 : MeasureTheory.Filtration ι m)
  {i : ι}, IsMax i → ↑𝓕.rightCont i = ↑𝓕 i
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- The natural transformation from identity functor to the composition of restriction and coextension
of scalars.
 -/
ModuleCat.RestrictionCoextensionAdj.unit' : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (f : R →+* S) →
          CategoryTheory.Functor.id (ModuleCat S) ⟶ (ModuleCat.restrictScalars f).comp (ModuleCat.coextendScalars f)
-- Mathlib.RepresentationTheory.Coinvariants
Representation.coinvariantsTprodLeftRegularLEquiv_symm_apply : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (a : V),
  ρ.coinvariantsTprodLeftRegularLEquiv.symm a =
    (Representation.Coinvariants.mk (ρ.tprod (Representation.leftRegular k G))) (a ⊗ₜ[k] MonoidAlgebra.single 1 1)
-- Mathlib.FieldTheory.Separable
Algebra.IsSeparable.of_algHom : ∀ (F : Type u_1) [inst : Field F] {E : Type u_3} (E' : Type u_4) [inst_1 : Field E] [inst_2 : Field E']
  [inst_3 : Algebra F E] [inst_4 : Algebra F E'] (f : E →ₐ[F] E') [Algebra.IsSeparable F E'], Algebra.IsSeparable F E
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.liftCycles_i_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0)
  [inst_2 : S.HasLeftHomology] {Z : C} (h : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.liftCycles k hk) (CategoryTheory.CategoryStruct.comp S.iCycles h) =
    CategoryTheory.CategoryStruct.comp k h
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.FibrantBrownFactorization.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  {f : X ⟶ Y} [inst_2 : SizeOf C]
  (toMapFactorizationData :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f)
  (r : toMapFactorizationData.Z ⟶ X)
  (i_r :
    autoParam (CategoryTheory.CategoryStruct.comp toMapFactorizationData.i r = CategoryTheory.CategoryStruct.id X)
      HomotopicalAlgebra.FibrantBrownFactorization.i_r._autoParam)
  (fibration_r :
    autoParam (HomotopicalAlgebra.Fibration r) HomotopicalAlgebra.FibrantBrownFactorization.fibration_r._autoParam),
  sizeOf { toMapFactorizationData := toMapFactorizationData, r := r, i_r := i_r, fibration_r := fibration_r } =
    1 + sizeOf toMapFactorizationData + sizeOf r + sizeOf i_r + sizeOf fibration_r
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_eq_mp : ∀ {δ : Type u_4} (X : δ → Type u_6) [inst : (a : δ) → MeasurableSpace (X a)] {i i' : δ} (h : i = i'), Measurable ⋯.mp
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.C_0 : ∀ {R : Type u_1} [inst : Semiring R], SkewPolynomial.C 0 = 0
-- Mathlib.FieldTheory.LinearDisjoint
/-- If there are `F`-bases `{ u_i }`, `{ v_j }` of `A`, `B`, such that the products
`{ u_i * v_j }` are linearly independent over `F`, then `A` and `B` are linearly disjoint.  -/
IntermediateField.LinearDisjoint.of_basis_mul : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  {κ : Type u_1} {ι : Type u_2} (a : Module.Basis κ F ↥A) (b : Module.Basis ι F ↥B),
  (LinearIndependent F fun i => ↑(a i.1) * ↑(b i.2)) → A.LinearDisjoint ↥B
-- Mathlib.Topology.Algebra.Group.Basic
Topology.IsInducing.continuousNeg : ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace H] [ContinuousNeg H] {f : G → H},
  Topology.IsInducing f → (∀ (x : G), f (-x) = -f x) → ContinuousNeg G
-- Mathlib.Tactic.Linter.HaveILetI
/-- `haveI` behaves like `have`, but inlines the value instead of producing a `have` term.  -/
Mathlib.Linter.HaveILetI.tacticHaveI__ : Lean.ParserDescr
-- Mathlib.Algebra.Group.Basic
add_add_sub_cancel : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b c : G), a + c + (b - c) = a + b
-- Mathlib.Data.Quot
/-- `Quot.mk r` is a surjective function.  -/
Quot.mk_surjective : ∀ {α : Sort u_1} {r : α → α → Prop}, Function.Surjective (Quot.mk r)
-- Mathlib.Data.PNat.Xgcd
PNat.gcd_det_eq : ∀ (a b : ℕ+), a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- The inverse of an integral element in a subalgebra of a division ring over a field
also lies in that subalgebra.  -/
IsIntegral.inv_mem : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : DivisionRing S] [inst_2 : Algebra R S] {x : S}
  {A : Subalgebra R S}, IsIntegral R x → x ∈ A → x⁻¹ ∈ A
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_sub_two_pi : ∀ (x : ℂ), Complex.sin (x - 2 * ↑Real.pi) = Complex.sin x
-- Mathlib.Order.Sublattice
Sublattice.coe_inj : ∀ {α : Type u_2} [inst : Lattice α] {L M : Sublattice α}, ↑L = ↑M ↔ L = M
-- Mathlib.GroupTheory.Exponent
Subgroup.exponent_top : ∀ {G : Type u} [inst : Group G], Monoid.exponent ↥⊤ = Monoid.exponent G
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.equivOp_apply_coe : ∀ {M : Type u_2} [inst : MulOneClass M] (H : Submonoid M) (a : ↥H), ↑(H.equivOp a) = MulOpposite.op ↑a
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_le_iff_of_lt : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} {ω : Ω} [WellFoundedLT ι] {m : ι},
  ∀ i < m, MeasureTheory.hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
-- Mathlib.Order.PiLex
Pi.lt_toColex_update_self_iff : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i}
  [inst_1 : (i : ι) → PartialOrder (β i)] [WellFoundedGT ι], toColex x < toColex (Function.update x i a) ↔ x i < a
-- Init.Data.Array.Erase
Array.erase_append_right : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α} (ys : Array α),
  a ∉ xs → (xs ++ ys).erase a = xs ++ ys.erase a
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.coe_smul_linearMap : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {S : Type u_4}
  [inst_7 : Monoid S] [inst_8 : DistribMulAction S M] [inst_9 : SMulCommClass R S M]
  [inst_10 : LieDerivation.SMulBracketCommClass S L M] (r : S) (D : LieDerivation R L M), ↑(r • D) = r • ↑D
-- Mathlib.NumberTheory.Wilson
/-- **Wilson's Theorem**: For `n ≠ 1`, `(n-1)!` is congruent to `-1` modulo `n` iff n is prime.  -/
Nat.prime_iff_fac_equiv_neg_one : ∀ {n : ℕ}, n ≠ 1 → (Nat.Prime n ↔ ↑(n - 1).factorial = -1)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.adjoint_toSpanSingleton : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] (x : E), LinearMap.adjoint (LinearMap.toSpanSingleton 𝕜 E x) = (innerₛₗ 𝕜) x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.map_id_equiv : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β},
  (Std.DHashMap.map (fun x v => v) m).Equiv m
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasDerivAt.csin : ∀ {f : ℂ → ℂ} {f' x : ℂ}, HasDerivAt f f' x → HasDerivAt (fun x => Complex.sin (f x)) (Complex.cos (f x) * f') x
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.xa.sizeOf_spec : ∀ {n : ℕ} (a : ZMod (2 * n)), sizeOf (QuaternionGroup.xa a) = 1 + sizeOf a
-- Init.Meta.Defs
Lean.Meta.CheckTactic.CheckGoalType.intro : ∀ {α : Sort u} (val : α), Lean.Meta.CheckTactic.CheckGoalType val
-- Mathlib.Computability.Language
Language.instMulRightMono : ∀ {α : Type u_1}, MulRightMono (Language α)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
CategoryTheory.ObjectProperty.le_colimitsCardinalClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (κ : Cardinal.{w}),
  P ≤ P.colimitsCardinalClosure κ
-- Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
MonoidAlgebra.instHopfAlgebra.eq_1 : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] {G : Type u_3}
  [inst_3 : Group G],
  MonoidAlgebra.instHopfAlgebra =
    { toHopfAlgebraStruct := MonoidAlgebra.instHopfAlgebraStruct R A G, mul_antipode_rTensor_comul := ⋯,
      mul_antipode_lTensor_comul := ⋯ }
-- Mathlib.CategoryTheory.Limits.Preorder
/-- If the point of cocone is a lub, the cocone is a .colimit  -/
Preorder.isColimitOfIsLUB : {C : Type u} →
  [inst : Preorder C] →
    {J : Type u'} →
      [inst_1 : CategoryTheory.Category.{v, u'} J] →
        (F : CategoryTheory.Functor J C) →
          (c : CategoryTheory.Limits.Cocone F) → IsLUB (Set.range F.obj) c.pt → CategoryTheory.Limits.IsColimit c
-- Init.Data.SInt.Lemmas
Int32.toBitVec_add : ∀ {a b : Int32}, (a + b).toBitVec = a.toBitVec + b.toBitVec
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_div_div₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Div β] [MeasurableDiv₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.IndepFun (f i / f j) (f k / f l) μ
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.replaceEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys (Std.Internal.List.replaceEntry k v l)
-- Mathlib.Data.Finset.Card
Finset.strongDownwardInduction.eq_def : ∀ {α : Type u_1} {p : Finset α → Sort u_4} {n : ℕ}
  (H : (t₁ : Finset α) → ({t₂ : Finset α} → t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁) (x : Finset α),
  Finset.strongDownwardInduction H x =
    let s := x;
    H s fun {t} ht h =>
      have this := ⋯;
      have this := ⋯;
      Finset.strongDownwardInduction H t ht
-- Mathlib.GroupTheory.EckmannHilton
/-- Local notation for `m a b`.  -/
_private.Mathlib.GroupTheory.EckmannHilton.0.EckmannHilton.«term_<_>_» : Lean.TrailingParserDescr
-- Mathlib.Data.Fin.Tuple.Basic
Fin.repeat_comp_rev : ∀ {m n : ℕ} {α : Sort u_1} (a : Fin n → α), Fin.repeat m a ∘ Fin.rev = Fin.repeat m (a ∘ Fin.rev)
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
spectrum.algebraMap_eq_of_mem : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A],
  (∀ {a : A}, IsUnit a ↔ a ≠ 0) → ∀ {a : A} {z : ℂ}, z ∈ spectrum ℂ a → (algebraMap ℂ A) z = a
-- Mathlib.Data.List.Map2
List.map₂Left_eq_map₂Left' : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → Option β → γ) (as : List α) (bs : List β),
  List.map₂Left f as bs = (List.map₂Left' f as bs).1
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
AlgebraicGeometry.SurjectiveOnStalks.eq_stalkwise : @AlgebraicGeometry.SurjectiveOnStalks =
  AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] x => Function.Surjective ⇑x
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_ofNat : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) [inst_1 : n.AtLeastTwo], (OfNat.ofNat n).natDegree = 0
-- Mathlib.Order.SupIndep
iSupIndep_subsingleton : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] [Subsingleton ι] (t : ι → α), iSupIndep t
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_of_contains_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {k a : α} {v : β}, (m.insert k v).contains a = true → (k == a) = false → m.contains a = true
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_sdiff_sub_sum_sdiff : ∀ {ι : Type u_1} {G : Type u_3} {s₁ s₂ : Finset ι} [inst : AddCommGroup G] [inst_1 : DecidableEq ι] {f : ι → G},
  ∑ x ∈ s₂ \ s₁, f x - ∑ x ∈ s₁ \ s₂, f x = ∑ x ∈ s₂, f x - ∑ x ∈ s₁, f x
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.mk : ∀ {X : Type u_2} [inst : Dist X], (∀ (x y z : X), dist x z ≤ max (dist x y) (dist y z)) → IsUltrametricDist X
-- Mathlib.Tactic.Linter.OverlappingInstances
/-- Lints against data-carrying overlaps between instances in the local contexts of declarations.
 -/
_private.Mathlib.Tactic.Linter.OverlappingInstances.0.Mathlib.Linter.OverlappingInstances.overlappingInstances : Lean.Linter
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulETransformRight_fst : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Group α] (e : α) (x : Finset α × Finset α),
  (Finset.mulETransformRight e x).1 = x.1 ∪ MulOpposite.op e • x.1
-- Mathlib.ModelTheory.Types
/-- The set of all formulas true at a tuple in a structure forms a complete type.  -/
FirstOrder.Language.Theory.typeOf : {L : FirstOrder.Language} →
  (T : L.Theory) →
    {α : Type w} → {M : Type w'} → [inst : L.Structure M] → [Nonempty M] → [M ⊨ T] → (α → M) → T.CompleteType α
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.pointwise_vadd_eq_map : ∀ {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (v : V) (s : AffineSubspace k P),
  v +ᵥ s = AffineSubspace.map (↑(AffineEquiv.constVAdd k P v)) s
-- Mathlib.Logic.Equiv.Sum
/-- Combine a permutation of `α` and of `β` into a permutation of `α ⊕ β`.  -/
Equiv.Perm.sumCongr : {α : Type u_9} → {β : Type u_10} → Equiv.Perm α → Equiv.Perm β → Equiv.Perm (α ⊕ β)
-- Init.Data.BitVec.Lemmas
/-- If two bitvectors have different `msb`s, then unsigned comparison is determined by this bit  -/
BitVec.ult_eq_msb_of_msb_neq : ∀ {w : ℕ} {x y : BitVec w}, x.msb ≠ y.msb → x.ult y = y.msb
-- Batteries.Data.List.Basic
/-- Get the maximum element of a list.
If the given list is empty, returns `(default : α)` and produces a panic error message.  -/
List.max! : {α : Type u_1} → [Inhabited α] → [Max α] → List α → α
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.aedisjoint : ∀ {G : Type u_1} {α : Type u_2} [inst : Zero G] [inst_1 : VAdd G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : autoParam (MeasureTheory.Measure α) MeasureTheory.IsAddFundamentalDomain._auto_1},
  MeasureTheory.IsAddFundamentalDomain G s μ → Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) fun g => g +ᵥ s)
-- Mathlib.RingTheory.Ideal.Maps
RingHom.ker.congr_simp : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [rcf : RingHomClass F R S] (f f_1 : F), f = f_1 → RingHom.ker f = RingHom.ker f_1
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A]
  (X : CategoryTheory.SimplicialObject A),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X)
      (AlgebraicTopology.inclusionOfMooreComplexMap X) =
    AlgebraicTopology.DoldKan.PInfty
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.lift_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {Y : D}
  (F : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X))
  (h : ∀ (f : CategoryTheory.MonoOver Y), CategoryTheory.Mono (F.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom)
  {X_1 Y_1 : CategoryTheory.MonoOver Y} (f : X_1 ⟶ Y_1), ((CategoryTheory.MonoOver.lift F h).map f).hom = F.map f.hom
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.kernelForkOfFork_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Fork f g),
  CategoryTheory.Limits.Fork.ι (CategoryTheory.Preadditive.kernelForkOfFork c) = c.ι
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantTo.precomp : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J},
  F.IsEventuallyConstantTo i₀ → ∀ {j : J} (f : j ⟶ i₀), F.IsEventuallyConstantTo j
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex.sizeOf_spec : ∀ {n : ℕ}, sizeOf Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex = 1
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.isoEquivBialgEquiv_apply : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : CommRing X] [inst_2 : HopfAlgebra R X] [inst_3 : CommRing Y]
  [inst_4 : HopfAlgebra R Y]
  (i : { X := X, commRing := inst_1, hopfAlgebra := inst_2 } ≅ { X := Y, commRing := inst_3, hopfAlgebra := inst_4 }),
  CommHopfAlgCat.isoEquivBialgEquiv i = CommHopfAlgCat.ofIso i
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instantiateRevRangeArgs : {pu : Lean.Compiler.LCNF.Purity} → Lean.Expr → ℕ → ℕ → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Expr
-- Mathlib.Data.List.Defs
/-- `findM? p l` returns the first element `a` of `l` for which `p a` returns
true. `findM?` short-circuits, so `p` is not necessarily run on every `a` in
`l`. This is a monadic version of `List.find`.  -/
List.findM?' : {m : Type u → Type v} → [Monad m] → {α : Type u} → (α → m (ULift.{u, 0} Bool)) → List α → m (Option α)