mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Find
Array.of_findIdx?_eq_none : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool},
  Array.findIdx? p xs = none →
    ∀ (i : ℕ),
      match xs[i]? with
      | some a => ¬p a = true
      | none => true = true
-- Mathlib.FieldTheory.Separable
Algebra.IsSeparable.isIntegral : ∀ (F : Type u_1) {K : Type u_3} [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K] [Algebra.IsSeparable F K]
  (x : K), IsIntegral F x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.braiding_inv_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S : CategoryTheory.Over X},
  CategoryTheory.Over.Hom.left (β_ R S).inv = (CategoryTheory.Limits.pullbackSymmetry S.hom R.hom).hom
-- Mathlib.Analysis.SpecificLimits.Normed
tendsto_pow_atTop_nhds_zero_iff_norm_lt_one : ∀ {R : Type u_2} [inst : SeminormedRing R] [NormMulClass R] {x : R},
  Filter.Tendsto (fun n => x ^ n) Filter.atTop (nhds 0) ↔ ‖x‖ < 1
-- Mathlib.Order.OmegaCompletePartialOrder
/-- **Alias** of `OmegaCompletePartialOrder.Chain.coe_map`. -/
OmegaCompletePartialOrder.Chain.map_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (c : OmegaCompletePartialOrder.Chain α)
  (f : α →o β), ⇑(c.map f) = ⇑f ∘ ⇑c
-- Init.Data.UInt.Lemmas
UInt32.toUInt32_toUInt8 : ∀ (n : UInt32), n.toUInt8.toUInt32 = n % 256
-- Mathlib.Analysis.Convex.Function
concaveOn_of_convex_hypograph : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : Module 𝕜 β] {s : Set E}
  {f : E → β}, Convex 𝕜 {p | p.1 ∈ s ∧ p.2 ≤ f p.1} → ConcaveOn 𝕜 s f
-- Init.System.IO
/-- The assigned group's permissions to access the file.  -/
IO.FileRight.group : IO.FileRight → IO.AccessRight
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.T_pow_nonneg : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]} (n : ℕ), 0 ≤ T_gen✝ p F a ^ n
-- Mathlib.Data.Finset.Sups
Finset.sups_union_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s t₁ t₂ : Finset α},
  s ⊻ (t₁ ∪ t₂) = s ⊻ t₁ ∪ s ⊻ t₂
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- Transport an exact pairing across an isomorphism in the second argument.  -/
CategoryTheory.exactPairingCongrRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y Y' : C} → [CategoryTheory.ExactPairing X Y'] → (Y ≅ Y') → CategoryTheory.ExactPairing X Y
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.instTopOfBot.eq_1 : ∀ (α : Type u) [h : Bot α], OrderDual.instTopOfBot α = { top := ⊥ }
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.measure_sigmaFiniteSetGE_ge : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure ν]
  (n : ℕ),
  (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : MeasureTheory.SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤
    ν (μ.sigmaFiniteSetGE ν n)
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.mk.injEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (leftFun : E → F) (leftDeriv : E →L[𝕜] F) (rightFun : E → G)
  (rightDeriv : E →L[𝕜] G) (pt : E) (hasStrictFDerivAt_leftFun : HasStrictFDerivAt leftFun leftDeriv pt)
  (hasStrictFDerivAt_rightFun : HasStrictFDerivAt rightFun rightDeriv pt) (range_leftDeriv : (↑leftDeriv).range = ⊤)
  (range_rightDeriv : (↑rightDeriv).range = ⊤) (isCompl_ker : IsCompl (↑leftDeriv).ker (↑rightDeriv).ker)
  (leftFun_1 : E → F) (leftDeriv_1 : E →L[𝕜] F) (rightFun_1 : E → G) (rightDeriv_1 : E →L[𝕜] G) (pt_1 : E)
  (hasStrictFDerivAt_leftFun_1 : HasStrictFDerivAt leftFun_1 leftDeriv_1 pt_1)
  (hasStrictFDerivAt_rightFun_1 : HasStrictFDerivAt rightFun_1 rightDeriv_1 pt_1)
  (range_leftDeriv_1 : (↑leftDeriv_1).range = ⊤) (range_rightDeriv_1 : (↑rightDeriv_1).range = ⊤)
  (isCompl_ker_1 : IsCompl (↑leftDeriv_1).ker (↑rightDeriv_1).ker),
  ({ leftFun := leftFun, leftDeriv := leftDeriv, rightFun := rightFun, rightDeriv := rightDeriv, pt := pt,
        hasStrictFDerivAt_leftFun := hasStrictFDerivAt_leftFun,
        hasStrictFDerivAt_rightFun := hasStrictFDerivAt_rightFun, range_leftDeriv := range_leftDeriv,
        range_rightDeriv := range_rightDeriv, isCompl_ker := isCompl_ker } =
      { leftFun := leftFun_1, leftDeriv := leftDeriv_1, rightFun := rightFun_1, rightDeriv := rightDeriv_1, pt := pt_1,
        hasStrictFDerivAt_leftFun := hasStrictFDerivAt_leftFun_1,
        hasStrictFDerivAt_rightFun := hasStrictFDerivAt_rightFun_1, range_leftDeriv := range_leftDeriv_1,
        range_rightDeriv := range_rightDeriv_1, isCompl_ker := isCompl_ker_1 }) =
    (leftFun = leftFun_1 ∧ leftDeriv = leftDeriv_1 ∧ rightFun = rightFun_1 ∧ rightDeriv = rightDeriv_1 ∧ pt = pt_1)
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_comap_comap_eq_relfinrank_inf : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E),
  (IntermediateField.comap f A).relfinrank (IntermediateField.comap f B) = A.relfinrank (B ⊓ f.fieldRange)
-- Mathlib.Data.Nat.Cast.Defs
three_add_one_eq_four : ∀ {R : Type u_1} [inst : AddMonoidWithOne R], 3 + 1 = 4
-- Mathlib.LinearAlgebra.RootSystem.OfBilinear
/-- A vector `x` is reflective with respect to a bilinear form if multiplication by its norm is
injective, and for any vector `y`, the norm of `x` divides twice the inner product of `x` and `y`.
These conditions are what we need when describing reflection as a map taking `y` to
`y - 2 • (B x y) / (B x x) • x`.  -/
LinearMap.IsReflective : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (M →ₗ[R] M →ₗ[R] R) → M → Prop
-- Mathlib.Algebra.Ring.Commute
neg_one_pow_mul_eq_zero_iff : ∀ {R : Type u} [inst : Ring R] {a : R} {n : ℕ}, (-1) ^ n * a = 0 ↔ a = 0
-- Mathlib.Analysis.Complex.Norm
Complex.abs_re_div_norm_le_one : ∀ (z : ℂ), |z.re / ‖z‖| ≤ 1
-- Lean.Meta.Tactic.Grind.ForallProp
Lean.Meta.Grind.propagateExistsDown : Lean.Meta.Grind.Propagator
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.any.eq_2 : ∀ {α : Type u_1} (p : α → Bool) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  RBTree.RBNode.any p (RBTree.RBNode.node c l v r) = (p v || RBTree.RBNode.any p l || RBTree.RBNode.any p r)
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfSquareZero.dpow_of_two_le : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] (hI2 : I ^ 2 = 0)
  {n : ℕ}, 2 ≤ n → ∀ (a : A), (DividedPowers.OfSquareZero.dividedPowers hI2).dpow n a = 0
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
/-- Conditional expectation of a function, in L1. Its value is 0 if the function is not
integrable. The function-valued `condExp` should be used instead in most cases.  -/
MeasureTheory.condExpL1 : {α : Type u_1} →
  {F' : Type u_3} →
    [inst : NormedAddCommGroup F'] →
      [NormedSpace ℝ F'] →
        {m m0 : MeasurableSpace α} →
          (hm : m ≤ m0) →
            (μ : MeasureTheory.Measure α) →
              [MeasureTheory.SigmaFinite (μ.trim hm)] → (α → F') → ↥(MeasureTheory.Lp F' 1 μ)
-- Init.Data.BitVec.Lemmas
BitVec.toNat_zero : ∀ {w : ℕ}, (0#w).toNat = 0
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.IsPerfectCompl.right_top_iff : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {p : M →ₗ[R] N →ₗ[R] R} [inst_5 : p.IsPerfPair] {U : Submodule R M},
  p.IsPerfectCompl U ⊤ ↔ U = ⊤
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
Fintype.linearIndependent_iffₒₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : LinearOrder R] [CanonicallyOrderedAdd R] [AddRightReflectLE R] [IsCancelAdd M]
  [inst_7 : DecidableEq ι] [inst_8 : Fintype ι],
  LinearIndependent R v ↔ ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.CorePlotsOn.isPlot_const : ∀ {X : Type u_1} (self : DiffeologicalSpace.CorePlotsOn X) {n : ℕ} (x : X), self.isPlot fun x_1 => x
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.instQuasiCompactCoverForgetQc : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.propQCPrecoverage P) S),
  AlgebraicGeometry.QuasiCompactCover 𝒰.forgetQc.toPreZeroHypercover
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- The type of morphisms in `AlgCat R`.  -/
AlgCat.Hom : {R : Type u} → [inst : CommRing R] → AlgCat R → AlgCat R → Type v
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.equivOp_apply_coe : ∀ {M : Type u_2} [inst : Mul M] (H : Subsemigroup M) (a : ↥H), ↑(H.equivOp a) = MulOpposite.op ↑a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_union_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β}, k ∉ t₂ → (t₁ \ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasStrictFDerivAt.sinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => Real.sinh (f x)) (Real.cosh (f x) • f') x
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.comp_injective_left : ∀ {V : Type u} [inst : Quiver V] {a b c : V} (q : Quiver.Path b c), Function.Injective fun p => p.comp q
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series expansion, then it is exponentially close to the partial
sums of this power series on strict subdisks of the disk of convergence.

This version provides an upper estimate that decreases both in `‖y‖` and `n`. See also
`HasFPowerSeriesWithinOnBall.uniform_geometric_approx` for a weaker version.  -/
HasFPowerSeriesWithinOnBall.uniform_geometric_approx' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} {r' : NNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    ↑r' < r →
      ∃ a ∈ Set.Ioo 0 1,
        ∃ C > 0,
          ∀ y ∈ Metric.ball 0 ↑r',
            ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
-- Mathlib.Topology.Order.LeftRightLim
Monotone.tendsto_rightLim_within : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f →
    ∀ [inst_4 : TopologicalSpace α] [OrderTopology α] (x : α),
      Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhdsWithin (Function.rightLim f x) (Set.Ici (Function.rightLim f x)))
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.mono : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
  {l l' : Filter α}, f =Θ[l] g → l' ≤ l → f =Θ[l'] g
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin_fst_of_lt_lt : ∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a b : α) (j : ℕ),
  0 < j → ∀ (hj₂ : j - 1 < k), (F.intervalGapsWithin h a b ↑j).1 = ((F.orderEmbOfFin h) ⟨j - 1, hj₂⟩).2
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} {fallback : β},
  Std.DTreeMap.Const.getD (Std.DTreeMap.filter f t) k fallback =
    ((Std.DTreeMap.Const.get? t k).pfilter fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.Plus.toPlus_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [inst_3 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_5 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} (S : J.Cover X) (x : CategoryTheory.ToType (P.obj (Opposite.op X))),
  (CategoryTheory.ConcreteCategory.hom ((J.toPlus P).app (Opposite.op X))) x =
    CategoryTheory.GrothendieckTopology.Plus.mk (CategoryTheory.Meq.mk S x)
-- Mathlib.Algebra.CharP.MixedCharZero
MixedCharZero.mk : ∀ {R : Type u_1} [inst : CommRing R] {p : ℕ} [toCharZero : CharZero R],
  (∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p) → MixedCharZero R p
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- A wrapper for `omega` which prefaces it with some quick and useful attempts  -/
CategoryTheory.ComposableArrows.tacticValid : Lean.ParserDescr
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Functor.map_inv_hom'_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ≅ Y) {F_1 : D → D → Type uF} {carrier : D → Type w}
  {instFunLike : (X Y : D) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory D F_1]
  (x : carrier (F.obj Y)),
  (CategoryTheory.ConcreteCategory.hom (F.map f.hom)) ((CategoryTheory.ConcreteCategory.hom (F.map f.inv)) x) = x
-- Std.Data.DTreeMap.Internal.Operations
/-- Monadic version of `map`.
 -/
Std.DTreeMap.Internal.Impl.mapM : {α : Type v} →
  {β γ : α → Type v} →
    {M : Type v → Type w} →
      [Applicative M] → ((a : α) → β a → M (γ a)) → Std.DTreeMap.Internal.Impl α β → M (Std.DTreeMap.Internal.Impl α γ)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.ne_zero : ∀ {k : ℕ} {M₀ : Type u_7} [inst : CommMonoidWithZero M₀] [Nontrivial M₀] {ζ : M₀}, IsPrimitiveRoot ζ k → k ≠ 0 → ζ ≠ 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {fallback : β} {f : β → β},
  Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.Const.modify m k f) k' fallback =
    if (k == k') = true then (Option.map f (Std.ExtDHashMap.Const.get? m k)).getD fallback
    else Std.ExtDHashMap.Const.getD m k' fallback
-- Mathlib.Topology.Inseparable
inseparable_iff_specializes_and : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Inseparable x y ↔ x ⤳ y ∧ y ⤳ x
-- Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
Lean.Meta.Grind.Arith.CommRing.denoteNum : {M : Type → Type} →
  [Monad M] →
    [Lean.MonadError M] →
      [MonadLiftT Lean.MetaM M] →
        [Lean.Meta.Sym.Arith.MonadCanon M] → [Lean.Meta.Grind.Arith.CommRing.MonadRing M] → ℤ → M Lean.Expr
-- Init.Data.List.ToArray
List.flatMap_toArray_cons : ∀ {α : Type u_1} {β : Type u_2} (f : α → Array β) (a : α) (as : List α),
  Array.flatMap f (a :: as).toArray = f a ++ Array.flatMap f as.toArray
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
/-- Append `a` to `x : Fin n ↪ ofStabilizer G a`  to get an element of `Fin n.succ ↪ α`.  -/
SubMulAction.ofStabilizer.snoc : {G : Type u_1} →
  [inst : Group G] →
    {α : Type u_2} →
      [inst_1 : MulAction G α] → {a : α} → {n : ℕ} → (Fin n ↪ ↥(SubMulAction.ofStabilizer G a)) → Fin n.succ ↪ α
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.ext_iff : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι}
  {x y : RestrictedProduct (fun i => R i) (fun i => A i) 𝓕}, x = y ↔ ∀ (i : ι), x i = y i
-- Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
CategoryTheory.Limits.pointwiseBinaryBicone_pt_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u_2} [inst_3 : CategoryTheory.Category.{v_2, u_2} D]
  (F G : CategoryTheory.Functor D C) (P : D),
  (CategoryTheory.Limits.pointwiseBinaryBicone F G).pt.obj P = (F.obj P ⊞ G.obj P)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.union_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp}, t₁.union t₂ = t₁ ∪ t₂
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for ensuring `BitVec.ofNat` literals are normalized.  -/
BitVec.reduceOfNat : Lean.Meta.Simp.DSimproc
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- If `(a : ℕ)` is a root of `cyclotomic n (ZMod p)`, where `p` is a prime, then `a` and `p` are
coprime.  -/
Polynomial.coprime_of_root_cyclotomic : ∀ {n : ℕ},
  0 < n →
    ∀ {p : ℕ} [hprime : Fact (Nat.Prime p)] {a : ℕ},
      (Polynomial.cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a) → a.Coprime p
-- Mathlib.RingTheory.Coalgebra.Hom
/-- If `φ : A → B` is a coalgebra map and `a = ∑ xᵢ ⊗ yᵢ`, then `φ a = ∑ φ xᵢ ⊗ φ yᵢ`
 -/
Coalgebra.Repr.induced : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      {ι : Type u_1} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid A] →
            [inst_2 : AddCommMonoid B] →
              [inst_3 : Module R A] →
                [inst_4 : Module R B] →
                  [inst_5 : Coalgebra R A] →
                    [inst_6 : Coalgebra R B] →
                      {a : A} →
                        Coalgebra.Repr R a ι →
                          {F : Type u_2} →
                            [inst_7 : FunLike F A B] → [CoalgHomClass F R A B] → (φ : F) → Coalgebra.Repr R (φ a) ι
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_minKey?_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.contains k = true → t.minKey?.isSome = true
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.hasCoeOpens : {G : Type u_1} →
  [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → CoeTC (OpenAddSubgroup G) (TopologicalSpace.Opens G)
-- Mathlib.Algebra.DirectSum.Module
/-- Coercion from a `DirectSum` to a pi type is a `LinearMap`.  -/
DirectSum.coeFnLinearMap : (R : Type u) →
  [inst : Semiring R] →
    {ι : Type v} →
      {M : ι → Type w} →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] → (DirectSum ι fun i => M i) →ₗ[R] (i : ι) → M i
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_nsmul_coe_pi : 2 • ↑Real.pi = 0
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.get!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α] (a : α)
  [inst_3 : Inhabited (β a)] (size : ℕ) (buckets : Array (Std.DHashMap.Internal.AssocList α β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.get! ⟨{ size := size, buckets := buckets }, hm⟩ a =
    Std.DHashMap.Internal.AssocList.getCast! a buckets[↑(Std.DHashMap.Internal.mkIdx buckets.size hm (hash a))]
-- Lean.Parser.Term
/-- A state monad that uses an actual mutable reference cell (i.e. an `ST.Ref`).

This is syntax, rather than a function, to make it easier to use. Its elaborator synthesizes an
appropriate parameter for the underlying monad's `ST` effects, then passes it to `StateRefT'`.
 -/
Lean.Parser.Term.stateRefT : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.natLinear : ∀ {C : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive],
  CategoryTheory.Functor.Linear ℕ F
-- Mathlib.NumberTheory.FrobeniusNumber
Nat.addSubmonoid_fg : ∀ (s : AddSubmonoid ℕ), s.FG
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_const_sub' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} (c : F), (deriv fun x => c - f x) = fun x => -deriv f x
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.zmod_intCast : ∀ (n : ℕ) [inst : NeZero n] (x y : ℤ), (AddChar.zmod n ↑x) ↑y = Circle.exp (2 * Real.pi * (↑x * ↑y / ↑n))
-- Lean.Util.NumApps
Lean.Expr.NumApps.main : Lean.Expr → Lean.NameMap ℕ
-- Mathlib.Order.Filter.AtTopBot.Disjoint
Filter.disjoint_pure_atBot : ∀ {α : Type u_3} [inst : Preorder α] [NoBotOrder α] (x : α), Disjoint (pure x) Filter.atBot
-- Mathlib.Topology.Metrizable.Uniformity
/-- If `X` is a uniform space with countably generated uniformity filter, there exists a
`PseudoMetricSpace` structure compatible with the `UniformSpace` structure. Use
`UniformSpace.pseudoMetricSpace` or `UniformSpace.metricSpace` instead.  -/
UniformSpace.metrizable_uniformity : ∀ (X : Type u_2) [inst : UniformSpace X] [(uniformity X).IsCountablyGenerated],
  ∃ I, PseudoMetricSpace.toUniformSpace = inst
-- Mathlib.Analysis.Complex.JensenFormula
circleAverage_re_herglotzRieszKernel_mul_log₀ : ∀ {w ρ : ℂ} {R : ℝ},
  ρ ∈ Metric.sphere 0 R →
    w ∈ Metric.ball 0 R →
      Real.circleAverage (Complex.re ∘ herglotzRieszKernel 0 w • fun x => Real.log ‖x - ρ‖) 0 R = Real.log ‖w - ρ‖
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
/-- The type underlying the category used in the construction of the composition
of colimit presentations. This is simply `Σ j, I j` but with a different category structure.  -/
CategoryTheory.Limits.ColimitPresentation.Total : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u_1} →
      {I : J → Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
          [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] →
            {D : CategoryTheory.Functor J C} →
              ((j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)) → Type (max u_2 u_1)
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftShortComplexFunctorIso_add'_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n m mn : ℤ)
  (hmn : m + n = mn) (a a' a'' : ℤ) (ha' : n + a = a') (ha'' : m + a' = a'') (K : CochainComplex C ℤ),
  (CochainComplex.shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K =
    CategoryTheory.CategoryStruct.comp
      ((HomologicalComplex.shortComplexFunctor C (ComplexShape.up ℤ) a).map
        ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K))
      (CategoryTheory.CategoryStruct.comp
        ((CochainComplex.shiftShortComplexFunctorIso C n a a' ha').hom.app
          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K))
        ((CochainComplex.shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K))
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.instCommRing : {q : ℕ} → CommRing (LucasLehmer.X q)