mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.toAlternatingMap_smul : ∀ {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [inst_4 : Monoid R']
  [inst_5 : Semiring A] [inst_6 : Module A M] [inst_7 : Module A N] [inst_8 : DistribMulAction R' N]
  [inst_9 : ContinuousConstSMul R' N] [inst_10 : SMulCommClass A R' N] (c : R') (f : M [⋀^ι]→L[A] N),
  (c • f).toAlternatingMap = c • f.toAlternatingMap
-- Mathlib.Analysis.Normed.Group.Continuity
Inseparable.nnnorm_eq_nnnorm : ∀ {E : Type u_4} [inst : SeminormedAddGroup E] {u v : E}, Inseparable u v → ‖u‖₊ = ‖v‖₊
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddCommSemigroup : {α : Type u_1} → [AddCommSemigroup α] → AddCommSemigroup (Colex α)
-- Init.Grind.Lemmas
Lean.Grind.and_eq_of_eq_false_right : ∀ {a b : Prop}, b = False → (a ∧ b) = False
-- Mathlib.Algebra.Homology.ComplexShape
/-- The `ComplexShape` appropriate for homology, so `d : X i ⟶ X j` only when `i = j + 1`.
 -/
ComplexShape.down : (α : Type u_2) → [inst : Add α] → [IsRightCancelAdd α] → [One α] → ComplexShape α
-- Mathlib.RingTheory.WittVector.Defs
WittVector.instZero : {p : ℕ} → {R : Type u_1} → [hp : Fact (Nat.Prime p)] → [CommRing R] → Zero (WittVector p R)
-- Init.System.Uri
System.Uri.UriEscape.letterA : UInt8
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofNNReal_toNNReal : ∀ (x : ℝ), ↑x.toNNReal = ENNReal.ofReal x
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_top : ExpGrowth.expGrowthInf ⊤ = ⊤
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.sum_measureReal_le_measureReal_univ : ∀ {α : Type u_1} {ι : Type u_3} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  {s : Finset ι} {t : ι → Set α},
  (∀ i ∈ s, MeasurableSet (t i)) → (↑s).PairwiseDisjoint t → ∑ i ∈ s, μ.real (t i) ≤ μ.real Set.univ
-- Mathlib.Analysis.LocallyConvex.Polar
StrongDual.polarSubmodule_eq_setOfPred : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] {S : Type u_6} [inst_4 : SetLike S E]
  [inst_5 : SMulMemClass S 𝕜 E] (m : S), ↑(StrongDual.polarSubmodule 𝕜 m) = {y | ∀ x ∈ m, y x = 0}
-- Lean.Elab.PatternVar
/-- Return the pattern variables in the given pattern.
Remark: this method is not used by the main `match` elaborator, but in the precheck hook and other macros (e.g., at `Do.lean`).
 -/
Lean.Elab.Term.getPatternVars : Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Elab.Term.PatternVar)
-- Mathlib.Logic.Small.Set
small_biInter : ∀ {α : Type u1} {ι : Type u4} {s : Set ι} {i : ι} (hi : i ∈ s) (f : (i : ι) → i ∈ s → Set α) [Small.{u, u1} ↑(f i hi)],
  Small.{u, u1} ↑(⋂ i, ⋂ (hi : i ∈ s), f i hi)
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.balance : ∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) r o₂ →
      (∃ l' r', Ordnode.BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')) →
        Ordnode.Valid' o₁ (l.balance x r) o₂
-- Mathlib.RingTheory.MvPowerSeries.LinearTopology
/-- If `J ≤ K` and `e ≤ d`, then we have the inclusion of two-sided ideals
`basis σ R ⟨J, d⟩ ≤ basis σ R ⟨K, e,>`.  -/
MvPowerSeries.LinearTopology.basis_le : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] {Jd Ke : TwoSidedIdeal R × (σ →₀ ℕ)},
  Jd.1 ≤ Ke.1 → Ke.2 ≤ Jd.2 → MvPowerSeries.LinearTopology.basis σ R Jd ≤ MvPowerSeries.LinearTopology.basis σ R Ke
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.AltParamInfo.mk.inj : ∀ {numFields numOverlaps : ℕ} {hasUnitThunk : Bool} {numFields_1 numOverlaps_1 : ℕ} {hasUnitThunk_1 : Bool},
  { numFields := numFields, numOverlaps := numOverlaps, hasUnitThunk := hasUnitThunk } =
      { numFields := numFields_1, numOverlaps := numOverlaps_1, hasUnitThunk := hasUnitThunk_1 } →
    numFields = numFields_1 ∧ numOverlaps = numOverlaps_1 ∧ hasUnitThunk = hasUnitThunk_1
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedMacroExpansionInfo.default : Lean.Elab.MacroExpansionInfo
-- Init.Data.List.Basic
List.replicateTR.loop : {α : Type u} → α → ℕ → List α → List α
-- Lean.Setup
Lean.instToJsonModuleHeader : Lean.ToJson Lean.ModuleHeader
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `MulSemiringActionHomClass F φ R S` states that `F` is a type of morphisms preserving
the ring structure and equivariant with respect to `φ`.

You should extend this class when you extend `MulSemiringActionHom`.  -/
MulSemiringActionSemiHomClass : (F : Type u_15) →
  {M : outParam (Type u_16)} →
    {N : outParam (Type u_17)} →
      [inst : Monoid M] →
        [inst_1 : Monoid N] →
          outParam (M → N) →
            (R : outParam (Type u_18)) →
              (S : outParam (Type u_19)) →
                [inst_2 : Semiring R] →
                  [inst_3 : Semiring S] → [DistribMulAction M R] → [DistribMulAction N S] → [FunLike F R S] → Prop
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.comp.inj : ∀ {a : Turing.ToPartrec.Code} {a_1 : Turing.PartrecToTM2.Cont'} {a_2 : Turing.ToPartrec.Code}
  {a_3 : Turing.PartrecToTM2.Cont'},
  Turing.PartrecToTM2.Cont'.comp a a_1 = Turing.PartrecToTM2.Cont'.comp a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.tensorRight_additive : ∀ {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] (X : C),
  (CategoryTheory.MonoidalCategory.tensorRight X).Additive
-- Mathlib.Data.Finset.Max
Finset.le_min : ∀ {α : Type u_2} [inst : LinearOrder α] {m : WithTop α} {s : Finset α}, (∀ a ∈ s, m ≤ ↑a) → m ≤ s.min
-- Mathlib.MeasureTheory.SetSemiring
/-- A ring of sets `C` is a family of sets containing `∅`, stable by union and set difference.
It is then also stable by intersection (see `IsSetRing.inter_mem`).  -/
MeasureTheory.IsSetRing : {α : Type u_1} → Set (Set α) → Prop
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.inverseImage (CategoryTheory.Functor.id C) = P
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
/-- Internal implementation detail of the `flatMap` combinator  -/
Std.Iterators.Types.Flatten : Type w → Type w → Type w → (Type w → Type u_1) → Type w
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
/-- Given an embedding `e : c.Embedding c'` of complex shapes, this is
the functor `HomotopyCategory C c ⥤ HomotopyCategory C c'` which
extend complexes along `e`.  -/
ComplexShape.Embedding.extendHomotopyFunctor : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          [e.IsRelIff] →
            (C : Type u_3) →
              [inst : CategoryTheory.Category.{v_1, u_3} C] →
                [CategoryTheory.Limits.HasZeroObject C] →
                  [inst_2 : CategoryTheory.Preadditive C] →
                    CategoryTheory.Functor (HomotopyCategory C c) (HomotopyCategory C c')
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- Given `R : ℝ` and `w : ℂ`, the canonical factor is the function
`fun z ↦ (R ^ 2 - (conj w) * z) / (R * (z - w))`. In applications, one will typically consider a
setting where `w ∈ ball 0 R`.
 -/
Complex.canonicalFactor : ℝ → ℂ → ℂ → ℂ
-- Mathlib.Algebra.Module.Equiv.Basic
LinearMap.funLeft_comp : ∀ (R : Type u_1) (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m : Type u_9}
  {n : Type u_10} {p : Type u_11} (f₁ : n → p) (f₂ : m → n),
  LinearMap.funLeft R M (f₁ ∘ f₂) = LinearMap.funLeft R M f₂ ∘ₗ LinearMap.funLeft R M f₁
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.convexCombPair_symm : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {x y : M},
  Convexity.convexCombPair s t hs ht h x y = Convexity.convexCombPair t s ht hs ⋯ y x
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Polynomial.monicEquivDegreeLT.congr_simp : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Nontrivial R] (n : ℕ),
  Polynomial.monicEquivDegreeLT n = Polynomial.monicEquivDegreeLT n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.self_le_maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {kmi : α}, (t.insert k v).maxKey?.get ⋯ = kmi → (cmp k kmi).isLE = true
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.notMem_disjointOfDiff : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C),
  t ∉ hC.disjointOfDiff hs ht
-- Std.Time.Time.PlainTime
/-- `Hour` component of the `PlainTime`
 -/
Std.Time.PlainTime.hour : Std.Time.PlainTime → Std.Time.Hour.Ordinal
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_X_pow_mul' : ∀ {R : Type u_1} [inst : Semiring R] (p : PowerSeries R) (n d : ℕ),
  (PowerSeries.coeff d) (PowerSeries.X ^ n * p) = if n ≤ d then (PowerSeries.coeff (d - n)) p else 0
-- Mathlib.Algebra.GroupWithZero.Pi
Pi.monoidWithZero : {ι : Type u_1} → {α : ι → Type u_2} → [(i : ι) → MonoidWithZero (α i)] → MonoidWithZero ((i : ι) → α i)
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_one_eq_bot : SimpleGraph.cycleGraph 1 = ⊥
-- Mathlib.Order.BoundedOrder.Lattice
inf_top_eq : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (a : α), a ⊓ ⊤ = a
-- Mathlib.Data.PNat.Xgcd
/-- `IsReduced` holds if the two entries in the vector are the
same.  The reduction algorithm will produce a system with this
property, whose product vector is the same as for the original
system.  -/
PNat.XgcdType.IsReduced : PNat.XgcdType → Prop
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- The isomorphism from a subgraph of `A` to its map under a copy `f : Copy A B`.  -/
SimpleGraph.Copy.isoSubgraphMap : {α : Type u_4} →
  {β : Type u_5} →
    {A : SimpleGraph α} →
      {B : SimpleGraph β} → (f : A.Copy B) → (A' : A.Subgraph) → A'.coe ≃g (SimpleGraph.Subgraph.map f.toHom A').coe
-- Mathlib.Data.Finset.Sups
Finset.infs_union_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s₁ s₂ t : Finset α},
  (s₁ ∪ s₂) ⊼ t = s₁ ⊼ t ∪ s₂ ⊼ t
-- Mathlib.RingTheory.Multiplicity
multiplicity_le_of_emultiplicity_le : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {n : ℕ}, emultiplicity a b ≤ ↑n → multiplicity a b ≤ n
-- Mathlib.Analysis.Normed.Group.Basic
mul_mem_closedBall_mul_iff : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a b : E} {r : ℝ} {c : E},
  a * c ∈ Metric.closedBall (b * c) r ↔ a ∈ Metric.closedBall b r
-- Lean.Meta.Tactic.Grind.EMatchTheoremParam
/-- Returns the number of digits needed to distinguish between different anchors.
 -/
Lean.Meta.Grind.getNumDigitsForLocalTheoremAnchors : Lean.Meta.Grind.Goal → Lean.Meta.Grind.GrindM ℕ
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_xor : ∀ (a b : ISize) (h : System.Platform.numBits = 64), (a ^^^ b).toBitVec64 h = a.toBitVec64 h ^^^ b.toBitVec64 h
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC_nc.go.eq_def : ∀ (c : ℕ) (a : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.toPolyC_nc.go c a =
    match a with
    | Lean.Grind.CommRing.Expr.num k => Lean.Grind.CommRing.Poly.num (k % ↑c)
    | Lean.Grind.CommRing.Expr.natCast k => Lean.Grind.CommRing.Poly.num (↑k % ↑c)
    | Lean.Grind.CommRing.Expr.intCast k => Lean.Grind.CommRing.Poly.num (k % ↑c)
    | Lean.Grind.CommRing.Expr.var x => Lean.Grind.CommRing.Poly.ofVar x
    | a.add b => (Lean.Grind.CommRing.Expr.toPolyC_nc.go c a).combineC (Lean.Grind.CommRing.Expr.toPolyC_nc.go c b) c
    | a.mul b => (Lean.Grind.CommRing.Expr.toPolyC_nc.go c a).mulC_nc (Lean.Grind.CommRing.Expr.toPolyC_nc.go c b) c
    | a.neg => Lean.Grind.CommRing.Poly.mulConstC (-1) (Lean.Grind.CommRing.Expr.toPolyC_nc.go c a) c
    | a.sub b =>
      (Lean.Grind.CommRing.Expr.toPolyC_nc.go c a).combineC
        (Lean.Grind.CommRing.Poly.mulConstC (-1) (Lean.Grind.CommRing.Expr.toPolyC_nc.go c b) c) c
    | a.pow k =>
      bif k == 0 then Lean.Grind.CommRing.Poly.num 1
      else
        match a with
        | Lean.Grind.CommRing.Expr.num n => Lean.Grind.CommRing.Poly.num (n ^ k % ↑c)
        | Lean.Grind.CommRing.Expr.var x =>
          Lean.Grind.CommRing.Poly.ofMon (Lean.Grind.CommRing.Mon.mult { x := x, k := k } Lean.Grind.CommRing.Mon.unit)
        | x => (Lean.Grind.CommRing.Expr.toPolyC_nc.go c a).powC_nc k c
-- Init.PropLemmas
exists_eq_or_imp : ∀ {α : Sort u_1} {p q : α → Prop} {a' : α}, (∃ a, (a = a' ∨ q a) ∧ p a) ↔ p a' ∨ ∃ a, q a ∧ p a
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
/-- The map on residue fields induced by a local homomorphism between local rings  -/
IsLocalRing.ResidueField.map : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : IsLocalRing R] →
        [inst_2 : CommRing S] →
          [inst_3 : IsLocalRing S] →
            (f : R →+* S) → [IsLocalHom f] → IsLocalRing.ResidueField R →+* IsLocalRing.ResidueField S
-- Aesop.Builder.Apply
Aesop.RuleBuilder.apply : Aesop.RuleBuilder
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.erasePTR.go.eq_def : ∀ {α : Type u_1} (p : α → Bool) (l a : List α) (a_1 : Array α),
  List.erasePTR.go✝ p l a a_1 =
    match a, a_1 with
    | [], x => l
    | a :: l_1, acc => bif p a then acc.toListAppend l_1 else List.erasePTR.go✝ p l l_1 (acc.push a)
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub' : Real.binEntropy = fun p => p.negMulLog + (1 - p).negMulLog
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₁ = f.left.left
-- Mathlib.Combinatorics.SetFamily.LYM
/-- The **Lubell-Yamamoto-Meshalkin inequality**, also known as the **LYM inequality**.

If `𝒜` is an antichain, then the sum of the proportion of elements it takes from each layer is less
than `1`.  -/
Finset.sum_card_slice_div_choose_le_one : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : Fintype α] {𝒜 : Finset (Finset α)},
  IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜 →
    ∑ r ∈ Finset.range (Fintype.card α + 1), ↑(𝒜.slice r).card / ↑((Fintype.card α).choose r) ≤ 1
-- Init.Data.Float.Model.Float32
Float32.instDecidableEqModel.decEq : (x x_1 : Float32.Model) → Decidable (x = x_1)
-- Mathlib.Topology.MetricSpace.Infsep
Set.Finite.infsep_exists_of_nontrivial : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α},
  s.Finite → s.Nontrivial → ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y
-- Lean.Parser.Extension
_private.Lean.Parser.Extension.0.Lean.Parser.throwParserCategoryAlreadyDefined : {α : Type} → Lean.Name → ExceptT String Id α
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.comp_apply : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [inst : NormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : NormedField 𝕜₂] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] (q : SeminormFamily 𝕜₂ F ι) (i : ι)
  (f : E →ₛₗ[σ₁₂] F), q.comp f i = (q i).comp f
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
/-- **Sturm bound for level-1 modular forms.** If a modular form `f` of weight `k` for `SL(2, ℤ)`
has q-expansion of order strictly greater than `k / 12`, then `f` is identically zero.
Corollary of the natural-weight version `sturm_bound_levelOne_nat`.  -/
ModularForm.sturm_bound_levelOne : ∀ {k : ℤ} {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k},
  ↑(k.toNat / 12) < (UpperHalfPlane.qExpansion 1 ⇑f).order → f = 0
-- Mathlib.Algebra.Star.Subalgebra
/-- The actual `StarSubalgebra` obtained from an element of a type satisfying `SubsemiringClass`,
`SMulMemClass` and `StarMemClass`.  -/
StarSubalgebra.ofClass : {S : Type u_6} →
  {R : Type u_7} →
    {A : Type u_8} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : StarRing R] →
              [inst_4 : StarRing A] →
                [inst_5 : StarModule R A] →
                  [inst_6 : SetLike S A] →
                    [SubsemiringClass S A] → [SMulMemClass S R A] → [StarMemClass S A] → S → StarSubalgebra R A
-- Mathlib.Algebra.Order.Pi
Function.const_nonpos : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Preorder α] {a : α} [Nonempty β],
  Function.const β a ≤ 0 ↔ a ≤ 0
-- Init.Data.SInt.Lemmas
Int32.toInt16_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt16 = OfNat.ofNat n
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
gelfandStarTransform_symm_apply : ∀ (A : Type u_1) [inst : CommCStarAlgebra A] (a : C(↑(WeakDual.characterSpace ℂ A), ℂ)),
  (gelfandStarTransform A).symm a =
    (RingEquiv.ofBijective { toAlgHom := WeakDual.gelfandTransform ℂ A, map_star' := ⋯ } ⋯).symm a
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_ne_zero : ∀ {α : Type u_1} [Nonempty α], ENat.card α ≠ 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- The n-skeleton as an endofunctor on `SSet`.  -/
SSet.sk : ℕ → CategoryTheory.Functor SSet SSet
-- Mathlib.Analysis.Normed.Group.Basic
enorm_eq_zero' : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ENormedMonoid E] {a : E}, ‖a‖ₑ = 0 ↔ a = 1
-- Init.Data.String.Lemmas.Order
String.Pos.slice_lt_iff : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁},
  q.slice p₀ p₁ h₀ h₁ < p ↔ q < String.Pos.ofSlice p
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus_eq_support_sub : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : AddGroup N] (f g : α →₀ N),
  f.neLocus g = (f - g).support
-- Init.Internal.Order.Basic
Lean.Order.instCCPOPi : {α : Sort u} → {β : α → Sort v} → [(x : α) → Lean.Order.CCPO (β x)] → Lean.Order.CCPO ((x : α) → β x)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
BoundedVariationOn.tendsto_atBot_limUnder : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [CompleteSpace E]
  [hE : Nonempty E] {f : α → E},
  BoundedVariationOn f Set.univ → Filter.Tendsto f Filter.atBot (nhds (Filter.atBot.limUnder f))
-- Mathlib.MeasureTheory.Measure.Regular
/-- A regular measure is weakly regular in an R₁ space.  -/
MeasureTheory.Measure.Regular.weaklyRegular : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [R1Space α]
  [μ.Regular], μ.WeaklyRegular
-- Init.Data.UInt.Lemmas
UInt32.two_mul : ∀ {a : UInt32}, 2 * a = a + a
-- Mathlib.Order.MinMax
min_le_min_right : ∀ {α : Type u} [inst : LinearOrder α] {a b : α} (c : α), b ≤ a → min b c ≤ min a c
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.docKinds : Array Lean.SyntaxNodeKind
-- Init.Data.Array.MapIdx
Array.mem_zipIdx_iff_le_and_getElem?_sub : ∀ {α : Type u_1} {x : α × ℕ} {xs : Array α} {k : ℕ}, x ∈ xs.zipIdx k ↔ k ≤ x.2 ∧ xs[x.2 - k]? = some x.1
-- Batteries.Data.Random.MersenneTwister
Batteries.Random.MersenneTwister.instStreamStateBitVecWordSize : (cfg : Batteries.Random.MersenneTwister.Config) →
  Std.Stream (Batteries.Random.MersenneTwister.State cfg) (BitVec cfg.wordSize)
-- Lean.Util.PPExt
Lean.FormatWithInfos.mk : Std.Format → Lean.PrettyPrinter.InfoPerPos → Lean.FormatWithInfos
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_sub : ∀ {x : ℂ} (y z : ℂ), x ≠ 0 → x ^ (y - z) = x ^ y / x ^ z
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
ContDiff.rpow_const_of_ne : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {p : ℝ} {n : WithTop ℕ∞},
  ContDiff ℝ n f → (∀ (x : E), f x ≠ 0) → ContDiff ℝ n fun x => f x ^ p
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.size_eq_if_rcc : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxc.HasSize α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [Std.Rxc.IsAlwaysFinite α] [Std.Rxc.LawfulHasSize α],
  r.size =
    if r.lower ≤ r.upper then
      match Std.PRange.succ? r.lower with
      | none => 1
      | some next => (next...=r.upper).size + 1
    else 0
-- Mathlib.Data.DFinsupp.Notation
/-- `DFinsupp` elaborator for `single₀`.  -/
DFinsupp.Internal.elabSingle₀ : Lean.Elab.Term.TermElab
-- Mathlib.Algebra.Order.IsBotOne
min_eq_zero : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Zero α] [IsBotZeroClass α] {a b : α}, min a b = 0 ↔ a = 0 ∨ b = 0
-- Mathlib.RingTheory.PowerSeries.Ideal
PowerSeries.spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] {P : Ideal (PowerSeries R)} [P.IsPrime],
  Submodule.spanFinrank P ≤ Submodule.spanFinrank (Ideal.map PowerSeries.constantCoeff P) + 1
-- Mathlib.Tactic.Linarith.Frontend
_private.Mathlib.Tactic.Linarith.Frontend.0.Mathlib.Tactic.instEvalExprGlobalBranchingPreprocessor.unsafe_impl_2 : Lean.Expr → Lean.MetaM Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Functor.Elements.shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  (F : CategoryTheory.Functor C (Type w)) {X₁ X₂ : C} (f : X₁ ⟶ X₂) (u : F.Elements) {Z : Type w} (h : F.obj X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shrinkYoneda.{w, v₁, u₁}.map f).app (Opposite.op u.fst))
      (CategoryTheory.CategoryStruct.comp
        (TypeCat.ofHom fun t =>
          (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.shrinkYonedaObjObjEquiv t))) u.snd)
        h) =
    CategoryTheory.CategoryStruct.comp
      (TypeCat.ofHom fun t =>
        (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.shrinkYonedaObjObjEquiv t))) u.snd)
      (CategoryTheory.CategoryStruct.comp (F.map f) h)
-- Mathlib.Algebra.BigOperators.Group.List.Defs
List.sum_hom_rel : ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddMonoid M] [inst_1 : AddMonoid N] (l : List ι)
  {r : M → N → Prop} {f : ι → M} {g : ι → N},
  r 0 0 → (∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i + a) (g i + b)) → r (List.map f l).sum (List.map g l).sum
-- Mathlib.Data.ENat.Lattice
/-- If `a ≠ 0`, then right multiplication by `a` maps infimum to infimum.
See also `ENat.iInf_mul` that assumes `[Nonempty ι]` but does not require `a ≠ 0`.  -/
ENat.iInf_mul_of_ne : ∀ {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞}, a ≠ 0 → (⨅ i, f i) * a = ⨅ i, f i * a
-- Mathlib.Order.Interval.Basic
Interval.mem_pure_self : ∀ {α : Type u_1} [inst : PartialOrder α] (a : α), a ∈ Interval.pure a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_modify : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' fallback : α} {f : β → β},
  m.WF →
    (m.modify k f).getKeyD k' fallback =
      if (k == k') = true then if k ∈ m then k else fallback else m.getKeyD k' fallback
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
_private.Std.Tactic.BVDecide.LRAT.Internal.Clause.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.isUnit.match_1.splitter : {n : ℕ} →
  (motive : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1) →
    (x : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
      ((l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → motive [l]) →
        ((x : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
            (∀ (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)), x = [l] → False) → motive x) →
          motive x
-- Mathlib.Algebra.Category.AlgCat.Basic
CategoryTheory.Iso.toAlgEquiv_symm_apply : ∀ {R : Type u} [inst : CommRing R] {X Y : AlgCat R} (i : X ≅ Y) (a : ↑Y),
  i.toAlgEquiv.symm a = (CategoryTheory.ConcreteCategory.hom i.inv) a