mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- **Alias** of `LinearMap.BilinForm.nondegenerate_flip_iff`. -/
LinearMap.BilinForm.nonDegenerateFlip_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.flip.Nondegenerate ↔ B.Nondegenerate
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τr : ∀ {a b c : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x : a ⟶ b) (x_1 : b ⟶ c),
  (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x x_1).inv.τr =
    CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pushforwardComp x_1.as.unop x.as.unop).inv
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- An infinite place is ramified in a field extension if it is not unramified.
 -/
NumberField.InfinitePlace.IsRamified : (k : Type u_1) →
  [inst : Field k] → {K : Type u_2} → [inst_1 : Field K] → [Algebra k K] → NumberField.InfinitePlace K → Prop
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.stabilizerEquivStabilizer.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g : G} {a b : α} (hg : b = g • a),
  MulAction.stabilizerEquivStabilizer hg =
    (MulEquiv.subgroupMap (MulAut.conj g) (MulAction.stabilizer G a)).trans (MulEquiv.subgroupCongr ⋯)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_neg : ∀ {R : Type u_1} [inst : Ring R] {p : SkewPolynomial R}, (-p).support = p.support
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.op_unop_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Fork f g), c.op.unop.ι = c.ι
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The isomorphism version of `leftZigzag`.  -/
CategoryTheory.Bicategory.leftZigzagIso : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f : a ⟶ b} →
        {g : b ⟶ a} →
          (CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g) →
            (CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b) →
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ≅
                CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b))
-- Mathlib.Topology.Algebra.Support
/-- If `f` has compact multiplicative support, then `f` tends to 1 at infinity.  -/
HasCompactMulSupport.is_one_at_infty : ∀ {α : Type u_2} {γ : Type u_5} [inst : TopologicalSpace α] [inst_1 : One γ] {f : α → γ} [inst_2 : TopologicalSpace γ],
  HasCompactMulSupport f → Filter.Tendsto f (Filter.cocompact α) (nhds 1)
-- Mathlib.RingTheory.Flat.Rank
/-- The rank is positive at all stalks if and only if the induced map on prime spectra is
surjective.  -/
PrimeSpectrum.rankAtStalk_pos_iff_comap_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S]
  [Module.Finite R S],
  (∀ (p : PrimeSpectrum R), 0 < Module.rankAtStalk S p) ↔ Function.Surjective (PrimeSpectrum.comap (algebraMap R S))
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.lintField : Lean.Syntax → Lean.Syntax → String → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Data.Num.ZNum
ZNum.zneg_pos : ∀ (n : PosNum), -ZNum.pos n = ZNum.neg n
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin'_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (M : Matrix m n R) (v : n → R), (Matrix.toLin' M) v = M.mulVec v
-- Mathlib.RingTheory.Ideal.Maps
/-- `I.comap f` is the preimage of `I` under `f`.  -/
Ideal.comap : {R : Type u} →
  {S : Type v} →
    {F : Type u_1} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] → [inst_2 : FunLike F R S] → F → [RingHomClass F R S] → Ideal S → Ideal R
-- Init.Data.String.OrderInstances
String.Pos.Raw.instLawfulOrderBEq : Std.LawfulOrderBEq String.Pos.Raw
-- Init.Data.List.Monadic
List.foldlM_filterMap : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} [inst : Monad m] [LawfulMonad m]
  {f : α → Option β} {g : γ → β → m γ} {l : List α} {init : γ},
  List.foldlM g init (List.filterMap f l) =
    List.foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init l
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_eq_some_getD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {fallback : β}, a ∈ t → t[a]? = some (t.getD a fallback)
-- Batteries.Recycling.RBTree.Basic
/-- Asserts that `t₁` and `t₂` have the same number of elements in the same order,
and `R` holds pairwise between them. The tree structure is ignored.
 -/
RBTree.RBNode.all₂ : {α : Type u_1} → {β : Type u_2} → (α → β → Bool) → RBTree.RBNode α → RBTree.RBNode β → Bool
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
/-- Applies the given function to the result of the contained `m`-monadic operation with a
proof that the postcondition property holds, returning another operation in `m`.
 -/
Std.Iterators.HetT.prun : {m : Type u_1 → Type u_2} →
  {α : Type u_3} → {β : Type u_1} → [Monad m] → (x : Std.Iterators.HetT m α) → ((a : α) → x.Property a → m β) → m β
-- Mathlib.Analysis.Polynomial.CauchyBound
Polynomial.cauchyBound_X_sub_C : ∀ {K : Type u_1} [inst : NormedDivisionRing K] (x : K), (Polynomial.X - Polynomial.C x).cauchyBound = ‖x‖₊ + 1
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.exists_multiset_roots : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] [inst_2 : DecidableEq R] {p : Polynomial R},
  p ≠ 0 → ∃ s, ↑s.card ≤ p.degree ∧ ∀ (a : R), Multiset.count a s = Polynomial.rootMultiplicity a p
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
_private.Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas.0.RootPairing.termα : Lean.ParserDescr
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubMulAction.closure_le : ∀ {R : Type u_1} {M : Type u_2} [inst : SMul R M] {s : Set M} {p : SubMulAction R M},
  SubMulAction.closure R s ≤ p ↔ s ⊆ ↑p
-- Mathlib.Data.Set.Prod
Set.prod_range_univ_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m₁ : α → γ}, Set.range m₁ ×ˢ Set.univ = Set.range fun p => (m₁ p.1, p.2)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotating the first vector by the angle between the two vectors results in an angle of 0.  -/
Orientation.oangle_rotation_oangle_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), o.oangle ((o.rotation (o.oangle x y)) x) y = 0
-- Mathlib.Algebra.Order.Module.Defs
smul_le_smul_of_nonneg_right : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero β] [SMulPosMono α β], a₁ ≤ a₂ → 0 ≤ b → a₁ • b ≤ a₂ • b
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.overEquivalence_counitIso_inv_app : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) (X_1 : TopologicalSpace.Opens ↥U),
  U.overEquivalence.counitIso.inv.app X_1 = CategoryTheory.eqToHom ⋯
-- Mathlib.Order.Hom.Basic
OrderIso.map_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] (f : α ≃o β) (x y : α),
  f (x ⊔ y) = f x ⊔ f y
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonWorkDoneProgressOptions.fromJson : Lean.Json → Except String Lean.Lsp.WorkDoneProgressOptions
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryLTD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : α × β}, t₁.Equiv t₂ → t₁.getEntryLTD k fallback = t₂.getEntryLTD k fallback
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.iterateRange_succ : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {f : M →ₗ[R] M}
  {n : ℕ}, f.iterateRange (n + 1) = Submodule.map f (f.iterateRange n)
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabSigma : Lean.PrettyPrinter.Delaborator.Delab
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.startsWithFollowedByNumber : String → String → Bool
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- If `f` has a formal power series on a ball bounded by `1`, then `f` is constant equal
to `f x` on the ball.  -/
HasFiniteFPowerSeriesOnBall.eq_const_of_bound_one : ∀ {𝕜 : 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}
  {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFiniteFPowerSeriesOnBall f pf x 1 r → ∀ y ∈ Metric.eball x r, f y = f x
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.whiskerLeft_iso_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c : CategoryTheory.Bicategory.Pith B} (x : a ⟶ b)
  (x_1 x_2 : b ⟶ c) (f : x_1 ⟶ x_2),
  (CategoryTheory.Bicategory.whiskerLeft x f).iso.inv = CategoryTheory.Bicategory.whiskerLeft x.of f.iso.inv
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.unzeroD_coe : ∀ {α : Type u} (d x : α), WithZero.unzeroD d ↑x = x
-- Mathlib.MeasureTheory.PiSystem
/-- Every measurable space (σ-algebra) forms a Dynkin system  -/
MeasurableSpace.DynkinSystem.ofMeasurableSpace : {α : Type u_3} → MeasurableSpace α → MeasurableSpace.DynkinSystem α
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.DecreasingBy.ref : Lean.Elab.DecreasingBy → Lean.Syntax
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The completed L-function of a Dirichlet character, almost everywhere equal to
`LFunction χ s * gammaFactor χ s`.
 -/
DirichletCharacter.completedLFunction : {N : ℕ} → [NeZero N] → DirichletCharacter ℂ N → ℂ → ℂ
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.whiskeringEquivalence`.

---

Whiskering by an equivalence gives an equivalence between categories of cones.
 -/
CategoryTheory.Limits.Cocones.whiskeringEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              (e : K ≌ J) → CategoryTheory.Limits.Cocone F ≌ CategoryTheory.Limits.Cocone (e.functor.comp F)
-- Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
compactlySupported_eq_top_iff : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : NonUnitalNormedRing γ] [Nontrivial γ],
  compactlySupported α γ = ⊤ ↔ IsCompact Set.univ
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.coe_one : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K), { toCompletion := ↑(WithAbs.toAbs (↑v) 1) } = 1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {a : α} [inst : Inhabited α], ∅.get! a = default
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- A continuous linear image of a bounded set is bounded.  -/
Bornology.IsVonNBounded.image : ∀ {E : Type u_3} {F : Type u_4} {𝕜₁ : Type u_6} {𝕜₂ : Type u_7} [inst : NormedDivisionRing 𝕜₁]
  [inst_1 : NormedDivisionRing 𝕜₂] [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F] {σ : 𝕜₁ →+* 𝕜₂}
  [RingHomSurjective σ] [RingHomIsometric σ] {s : Set E},
  Bornology.IsVonNBounded 𝕜₁ s → ∀ (f : E →SL[σ] F), Bornology.IsVonNBounded 𝕜₂ (⇑f '' s)
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
/-- Given a regular cardinal `κ`, a category `C` is `κ`-accessible
if it has `κ`-filtered colimits and admits a (small) family `G : ι → C` of `κ`-presentable
objects such that any object identifies as a `κ`-filtered colimit of these objects.  -/
CategoryTheory.IsCardinalAccessibleCategory : (C : Type u) → [CategoryTheory.Category.{v, u} C] → (κ : Cardinal.{w}) → [Fact κ.IsRegular] → Prop
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The order of the product of two formal power series
is at least the sum of their orders.  -/
MvPowerSeries.le_order_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f g : MvPowerSeries σ R}, f.order + g.order ≤ (f * g).order
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
UniformSpace.toTopologicalSpace.hcongr_2 : ∀ (α α' : Type u),
  α = α' →
    ∀ (self : UniformSpace α) (self' : UniformSpace α'),
      self ≍ self' → self.toTopologicalSpace ≍ self'.toTopologicalSpace
-- Mathlib.Algebra.Group.Finsupp
Finsupp.update_eq_erase_add_single : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (f : ι →₀ M) (a : ι) (b : M),
  f.update a b = Finsupp.erase a f + fun₀ | a => b
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.all_mapM : ∀ {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : MonadLiftT m n] [inst_3 : Std.IteratorLoop α m m] [inst_4 : Monad m]
  [LawfulMonad m] [inst_6 : Monad n] [inst_7 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [LawfulMonadLiftT m n] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {f : β → n β'} {p : β' → Bool},
  Std.IterM.all p (Std.IterM.mapM f it) =
    Std.IterM.allM (fun x => (fun x => { down := p x }) <$> f x) (Std.IterM.mapM pure it)
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.toTopologicalSpace_injective : ∀ {α : Type u} [inst : Group α], Function.Injective GroupTopology.toTopologicalSpace
-- Mathlib.Data.List.TakeDrop
List.takeI_length : ∀ {α : Type u} [inst : Inhabited α] (n : ℕ) (l : List α), (List.takeI n l).length = n
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.toZFSet_strictMono : StrictMono Ordinal.toZFSet
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.findIdx?_go_nil : ∀ {α : Type u_1} {p : α → Bool} {i : ℕ}, List.findIdx?.go p [] i = none
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.linearIndependent_h : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] (b : P.Base) [Finite ι] [CharZero R] [IsDomain R] [P.IsRootSystem],
  LinearIndependent R RootPairing.GeckConstruction.h
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (I J : CategoryTheory.InjectiveResolution X) {Z : CochainComplex C ℕ} (h : J.cocomplex ⟶ Z),
  CategoryTheory.CategoryStruct.comp I.ι (CategoryTheory.CategoryStruct.comp (I.homotopyEquiv J).hom h) =
    CategoryTheory.CategoryStruct.comp J.ι h
-- Std.Do.SPred.SVal
_private.Std.Do.SPred.SVal.0.Std.Do.SVal.uncurry.match_3.eq_2 : ∀ {α : Type u_1} (motive : (σs : List (Type u_1)) → Std.Do.SVal σs α → Sort u_2) (head : Type u_1)
  (tail : List (Type u_1)) (f : Std.Do.SVal (head :: tail) α) (h_1 : (f : Std.Do.SVal [] α) → motive [] f)
  (h_2 : (head : Type u_1) → (tail : List (Type u_1)) → (f : Std.Do.SVal (head :: tail) α) → motive (head :: tail) f),
  (match head :: tail, f with
    | [], f => h_1 f
    | head :: tail, f => h_2 head tail f) =
    h_2 head tail f
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Composition of morphisms in the indexing diagram for (co)equalizers.  -/
CategoryTheory.Limits.WalkingParallelPairHom.comp : {X Y Z : CategoryTheory.Limits.WalkingParallelPair} →
  CategoryTheory.Limits.WalkingParallelPairHom X Y →
    CategoryTheory.Limits.WalkingParallelPairHom Y Z → CategoryTheory.Limits.WalkingParallelPairHom X Z
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_one : ∀ (x : ℝ), x ^ 1 = x
-- Mathlib.RingTheory.Localization.FractionRing
FractionRing.unique : (R : Type u_1) → [inst : CommRing R] → [Subsingleton R] → Unique (FractionRing R)
-- Mathlib.Logic.Function.FromTypes
Function.fromTypes_cons_equiv_symm_apply : ∀ {n : ℕ} (α : Type u) (p : Fin n → Type u) (τ : Type u) (a : Function.FromTypes (Matrix.vecCons α p) τ),
  (Function.fromTypes_cons_equiv α p τ).symm a = a
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.toLoop.eq_1 : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N)
  (p : ↑(GenLoop N X x)),
  GenLoop.toLoop i p =
    { toFun := fun t => ⟨((↑p).comp ↑(Cube.insertAt i)).curry t, ⋯⟩, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
-- Mathlib.Tactic.Ring.Common
/-- Multiplies a monomial `va` to a polynomial `vb` to get a normalized result polynomial.

* `a * 0 = 0`
* `a * (b₁ + b₂) = (a * b₁) + (a * b₂)`
 -/
Mathlib.Tactic.Ring.Common.evalMul₁ : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
            {a b : Q(«$α»)} →
              Mathlib.Tactic.Ring.Common.ExProd bt sα a →
                Mathlib.Tactic.Ring.Common.ExSum bt sα b →
                  Lean.MetaM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum bt sα) q(«$a» * «$b»))
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension : ∀ {n : ℕ} {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.SmoothOfRelativeDimension n f]
  (x : ↥X),
  ∃ U,
    ∃ (_ : AlgebraicGeometry.IsAffineOpen U),
      ∃ V,
        ∃ (_ : AlgebraicGeometry.IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          RingHom.IsStandardSmoothOfRelativeDimension n
            (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e))
-- Init.Data.Nat.Fold
Nat.dfoldRev_succ : ∀ {n : ℕ} {α : (i : ℕ) → autoParam (i ≤ n + 1) Nat.dfoldRev_succ._auto_3 → Type u}
  (f : (i : ℕ) → (h : i < n + 1) → α (i + 1) ⋯ → α i ⋯) (init : α (n + 1) ⋯),
  (n + 1).dfoldRev f init = n.dfoldRev (fun i h => f i ⋯) (f n ⋯ init)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.Equiv.filterMapM : ∀ {α₁ α₂ β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [inst_1 : LawfulMonad m]
  [inst_2 : Monad n] [inst_3 : MonadAttach n] [inst_4 : LawfulMonad n] [inst_5 : Std.Iterator α₁ m β]
  [inst_6 : Std.Iterator α₂ m β] [inst_7 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n (Option γ)}
  {ita : Std.IterM m β} {itb : Std.IterM m β},
  ita.Equiv itb → (Std.IterM.filterMapM f ita).Equiv (Std.IterM.filterMapM f itb)
-- Init.Data.BitVec.Lemmas
BitVec.toFin_signExtend : ∀ {w v : ℕ} (x : BitVec w),
  (BitVec.signExtend v x).toFin = Fin.ofNat (2 ^ v) (x.toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0)
-- Init.Data.SInt.Lemmas
Int8.le_rfl : ∀ {a : Int8}, a ≤ a
-- Mathlib.Data.QPF.Multivariate.Basic
/-- Multivariate quotients of polynomial functors.
 -/
MvQPF : {n : ℕ} → (TypeVec.{u} n → Type u_1) → Type (max (u + 1) u_1)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_comp : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p]
  [ContinuousMapZero.UniqueHom R A] (g f : R → R) (a : A),
  autoParam (ContinuousOn g (f '' quasispectrum R a)) cfcₙ_comp._auto_1 →
    autoParam (g 0 = 0) cfcₙ_comp._auto_3 →
      autoParam (ContinuousOn f (quasispectrum R a)) cfcₙ_comp._auto_5 →
        autoParam (f 0 = 0) cfcₙ_comp._auto_7 → autoParam (p a) cfcₙ_comp._auto_9 → cfcₙ (g ∘ f) a = cfcₙ g (cfcₙ f a)
-- Mathlib.Data.Multiset.Functor
Multiset.naturality : ∀ {G H : Type u_1 → Type u_1} [inst : Applicative G] [inst_1 : Applicative H] [inst_2 : CommApplicative G]
  [inst_3 : CommApplicative H] (eta : ApplicativeTransformation G H) {α β : Type u_1} (f : α → G β) (x : Multiset α),
  (fun {α} => eta.app α) (Multiset.traverse f x) = Multiset.traverse ((fun {α} => eta.app α) ∘ f) x
-- Mathlib.Data.Num.Basic
PosNum.one.sizeOf_spec : sizeOf PosNum.one = 1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.mem_supp_of_adj_mem_supp : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V}, u ∈ C.supp → G.Adj u v → v ∈ C.supp
-- Mathlib.Control.Random
/-- A monad transformer to generate random objects using the generator type `StdGen`.
`RandT m α` should be thought of a random value in `m α`.  -/
RandT : (Type u_1 → Type u_2) → Type u_1 → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- Construct a cone on `F` from an object of the category `(Δ ↓ F)`. This is part of an
equivalence, see `Cone.equivCostructuredArrow`.  -/
CategoryTheory.Limits.Cone.fromCostructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) →
          CategoryTheory.Functor (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F)
            (CategoryTheory.Limits.Cone F)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasProd_subtype_mulSupport : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α},
  HasProd (f ∘ Subtype.val) a ↔ HasProd f a
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The functor `fun X ↦ X ⊗ 𝟙_ C`.  -/
CategoryTheory.MonoidalCategory.tensorUnitRight : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → CategoryTheory.Functor C C
-- Init.Data.String.FindPos
/-- Returns the previous valid position before the given position, given a proof that the position
is not the start position, which guarantees that such a position exists.  -/
String.Pos.prev : {s : String} → (pos : s.Pos) → pos ≠ s.startPos → s.Pos
-- Init.Data.Bool
Bool.true_bne : ∀ (b : Bool), (true != b) = !b
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.appendText : {α : Type u_1} → String → Lean.Widget.TaggedText α → Lean.Widget.TaggedText α
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.map_comp_eq : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G H : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G) (β : G ⟶ H),
  CategoryTheory.Pseudofunctor.Grothendieck.map (CategoryTheory.CategoryStruct.comp α β) =
    (CategoryTheory.Pseudofunctor.Grothendieck.map α).comp (CategoryTheory.Pseudofunctor.Grothendieck.map β)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.decl.injEq : ∀ (xs : Array Lean.Elab.Term.Do.Var) (doElem : Lean.Syntax) (k : Lean.Elab.Term.Do.Code)
  (xs_1 : Array Lean.Elab.Term.Do.Var) (doElem_1 : Lean.Syntax) (k_1 : Lean.Elab.Term.Do.Code),
  (Lean.Elab.Term.Do.Code.decl xs doElem k = Lean.Elab.Term.Do.Code.decl xs_1 doElem_1 k_1) =
    (xs = xs_1 ∧ doElem = doElem_1 ∧ k = k_1)
-- Std.Data.HashSet.Basic
/-- Checks if given key is contained and returns the key if it is, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the set.
 -/
Std.HashSet.get! : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → [Inhabited α] → Std.HashSet α → α → α