mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
IsStarNormal.cfc_map : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  IsStarNormal (cfc f a)
-- Init.Data.SInt.Bitwise
Int8.shiftLeft_and : ∀ {a b c : Int8}, (a &&& b) <<< c = a <<< c &&& b <<< c
-- Mathlib.Algebra.Group.Commute.Hom
addSemiconjBy_map_iff : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Add M] [inst_1 : Add N] {a : M} [inst_2 : FunLike F M N]
  [AddHomClass F M N] {f : F},
  Function.Injective ⇑f → ∀ {x y : M}, AddSemiconjBy (f a) (f x) (f y) ↔ AddSemiconjBy a x y
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.mem_eball'`. -/
EMetric.mem_ball' : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal}, y ∈ Metric.eball x ε ↔ edist x y < ε
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_mk : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (s : Multiset ι) (hs : s.Nodup) (f : ι → M),
  { val := s, nodup := hs }.sum f = (Multiset.map f s).sum
-- Std.Time.Time.Unit.Millisecond
/-- Creates an `Offset` from a natural number.
 -/
Std.Time.Millisecond.Offset.ofNat : ℕ → Std.Time.Millisecond.Offset
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.instIsProperPairingOfIsProper : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) [h.IsProper], h.pairing.IsProper
-- Std.Data.Iterators.Lemmas.Producers.Array
Array.toList_iterFromIdx : ∀ {β : Type w} {array : Array β} {pos : ℕ}, (array.iterFromIdx pos).toList = List.drop pos array.toList
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.Scheme.emptyTo_base : ∀ (X : AlgebraicGeometry.Scheme), X.emptyTo.base = TopCat.ofHom { toFun := fun x => x.elim, continuous_toFun := ⋯ }
-- Lean.MetavarContext
/-- The type of the metavariable, in the given `lctx`.  -/
Lean.MetavarDecl.type : Lean.MetavarDecl → Lean.Expr
-- Lean.Environment
/-- Checks whether `findAsync?` would return a result.

NOTE: Unlike `findAsync`, this function defaults `skipRealize` to `true` to avoid unnecessary
blocking on realizations, which should always be brought into scope by running `realizeConst`, which
does its own, optimized existence check.
 -/
Lean.Environment.contains : Lean.Environment → Lean.Name → optParam Bool true → Bool
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.instNNRatCast : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : DivisionRing β] →
            {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → NNRatCast (CauSeq.Completion.Cauchy abv)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coe_add : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f g : ρ.IntertwiningMap σ), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.zmod_add : ∀ {n : ℕ} [inst : NeZero n] (x y : ZMod n), AddChar.zmod n (x + y) = AddChar.zmod n x * AddChar.zmod n y
-- Mathlib.Analysis.Calculus.FDeriv.Comp
HasFDerivWithinAt.iterate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {f : E → E} {f' : E →L[𝕜] E},
  HasFDerivWithinAt f f' s x → f x = x → Set.MapsTo f s s → ∀ (n : ℕ), HasFDerivWithinAt f^[n] (f' ^ n) s x
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.sum_le_tsum : ∀ {α : Type u_1} {f : α → ENNReal} (s : Finset α), ∑ x ∈ s, f x ≤ ∑' (x : α), f x
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Over.w : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {A B : P.Over Q X} (f : A ⟶ B), CategoryTheory.CategoryStruct.comp f.left B.hom = A.hom
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.comp_le_of_monotoneOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {β : Type u_3}
  [inst_2 : LinearOrder β] (f : α → E) {s : Set α} {t : Set β} (φ : β → α),
  MonotoneOn φ t → Set.MapsTo φ t s → eVariationOn (f ∘ φ) t ≤ eVariationOn f s
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
ordinaryHypergeometricSeries_symm : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (a b c : 𝕂),
  ordinaryHypergeometricSeries 𝔸 a b c = ordinaryHypergeometricSeries 𝔸 b a c
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.neg_add_cancel : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F (x.neg.add x) CommRingCat.Colimits.Prequotient.zero
-- Mathlib.Algebra.Free
FreeMagma.instMonad.eq_1 : FreeMagma.instMonad =
  { map := fun {α β} f x => (fun {α β} x f => (FreeMagma.lift f) x) x ((fun {α} => FreeMagma.of) ∘ f),
    pure := fun {α} => FreeMagma.of,
    seq := fun {α β} f x =>
      (fun {α β} x f => (FreeMagma.lift f) x) f fun y =>
        (fun {α β} x f => (FreeMagma.lift f) x) (x ()) ((fun {α} => FreeMagma.of) ∘ y),
    seqLeft := fun {α β} x y =>
      (fun {α β} x f => (FreeMagma.lift f) x) x fun a =>
        (fun {α β} x f => (FreeMagma.lift f) x) (y ()) fun x => (fun {α} => FreeMagma.of) a,
    seqRight := fun {α β} x y => (fun {α β} x f => (FreeMagma.lift f) x) x fun x => y (),
    bind := fun {α β} x f => (FreeMagma.lift f) x }
-- Aesop.Frontend.Tactic
Aesop.Frontend.TacticConfig.erasedRules : Aesop.Frontend.TacticConfig → Array Aesop.Frontend.RuleExpr
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.instMonObjSpecAsOverSpec : {R A : CommRingCat} →
  [inst : Bialgebra ↑R ↑A] → CategoryTheory.MonObj ((AlgebraicGeometry.Spec A).asOver (AlgebraicGeometry.Spec R))
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.bisim_equiv : ∀ {P : PFunctor.{uA, uB}} (R : P.M → P.M → Prop),
  (∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)) →
    ∀ (x y : P.M), R x y → x = y
-- Mathlib.Topology.MetricSpace.Closeds
/-- **Alias** of `TopologicalSpace.Closeds.edist_eq`.

---

By definition, the edistance on `Closeds α` is given by the Hausdorff edistance  -/
EMetric.Closeds.edist_eq : ∀ {α : Type u_1} [inst : EMetricSpace α] {s t : TopologicalSpace.Closeds α}, edist s t = Metric.hausdorffEDist ↑s ↑t
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderiv_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {f g : M → E'},
  MDiffAt f z → MDiffAt g z → mfderiv% (f - g) z = mfderiv% f z - mfderiv% g z
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfLEArgs.isGE_compare : ∀ {α : Type u} (self : Std.Packages.LinearPreorderOfLEArgs α),
  let this := self.le;
  let this_1 := self.decidableLE;
  have this_2 := ⋯;
  let this_3 := self.ord;
  ∀ (a b : α), (compare a b).isGE = true ↔ b ≤ a
-- Lean.Language.Lean.Types
/-- State after successful importing.  -/
Lean.Language.Lean.HeaderProcessedState : Type
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_cons_of_true : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β},
  (k == a) = true → Std.Internal.List.getValue? a (⟨k, v⟩ :: l) = some v
-- Mathlib.RingTheory.Morita.Basic
/-- Isomorphic `R`-algebras are Morita equivalent.
 -/
MoritaEquivalence.ofAlgEquiv : {R : Type u₀} →
  [inst : CommSemiring R] →
    {A : Type u₁} →
      {B : Type u₂} →
        [inst_1 : Ring A] →
          [inst_2 : Algebra R A] → [inst_3 : Ring B] → [inst_4 : Algebra R B] → (A ≃ₐ[R] B) → MoritaEquivalence R A B
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Get the variable whose type the user selected.  -/
Mathlib.Tactic.ClickSuggestions.getHypIdent! : Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM Lean.Ident
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.nonsingular_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (a b : R),
  W'.Nonsingular ![a, b, 1] ↔ W'.toAffine.Nonsingular a b
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of two antitone functions is antitone.  -/
AntitoneOn.add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
  [AddLeftMono α] [AddRightMono α], AntitoneOn f s → AntitoneOn g s → AntitoneOn (fun x => f x + g x) s
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.of_exponent_le : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {α β : ↑unitInterval} {f : E → F} {a : E},
  ContDiffPointwiseHolderAt k α f a → β ≤ α → ContDiffPointwiseHolderAt k β f a
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Uniform structure of uniform convergence, declared as an instance on `α →ᵤ β`.
We will denote it `𝒰(α, β, uβ)` in the rest of this file.  -/
UniformFun.uniformSpace : (α : Type u_1) → (β : Type u_2) → [UniformSpace β] → UniformSpace (UniformFun α β)
-- Mathlib.Geometry.Manifold.SmoothEmbedding
/-- A `C^n` map `f : M → M'` is a smooth `C^n` embedding if it is a topological embedding
and a `C^n` immersion.  -/
Manifold.IsSmoothEmbedding : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E₁ : Type u_2} →
      {E₃ : Type u_4} →
        [inst_1 : NormedAddCommGroup E₁] →
          [inst_2 : NormedSpace 𝕜 E₁] →
            [inst_3 : NormedAddCommGroup E₃] →
              [inst_4 : NormedSpace 𝕜 E₃] →
                {H : Type u_6} →
                  {G : Type u_8} →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        ModelWithCorners 𝕜 E₁ H →
                          ModelWithCorners 𝕜 E₃ G →
                            {M : Type u_10} →
                              {N : Type u_12} →
                                [inst : TopologicalSpace M] →
                                  [ChartedSpace H M] →
                                    [inst : TopologicalSpace N] → [ChartedSpace G N] → WithTop ℕ∞ → (M → N) → Prop
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.restrictPreimage_toFun : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty) (z : ↑(proj ⁻¹' s)),
  ↑(e.restrictPreimage hs).toPartialEquiv z = (⟨proj ↑z, ⋯⟩, (↑e ↑z).2)
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_symm_fiber : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C)
  [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois A] (a b : (F.obj A).obj),
  (CategoryTheory.ConcreteCategory.hom
        (F.map ((CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois F A a).symm b).hom))
      a =
    b
-- Mathlib.MeasureTheory.Function.JacobianOneDim
/-- Change of variable formula for differentiable functions, set version: if a real function `f` is
monotone and differentiable on a measurable set `s`, then the measure of `f '' s` is given by the
integral of `f' x` on `s` .
Note that the measurability of `f '' s` is given by `MeasurableSet.image_of_monotoneOn`.  -/
MeasureTheory.lintegral_deriv_eq_volume_image_of_monotoneOn : ∀ {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
      MonotoneOn f s → ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) = MeasureTheory.volume (f '' s)
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- **Alias** of `AddSubmonoid.coe_finsetSum`. -/
AddSubmonoid.coe_finset_sum : ∀ {ι : Type u_4} {M : Type u_5} [inst : AddCommMonoid M] (S : AddSubmonoid M) (f : ι → ↥S) (s : Finset ι),
  ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Mathlib.Control.Bifunctor
Function.bicompl.bifunctor : {F : Type u₀ → Type u₁ → Type u₂} →
  [Bifunctor F] →
    (G : Type u_1 → Type u₀) → (H : Type u_2 → Type u₁) → [Functor G] → [Functor H] → Bifunctor (Function.bicompl F G H)
-- Mathlib.Data.Matrix.Basic
AlgEquiv.mopMatrix_apply : ∀ {m : Type u_2} {R : Type u_7} {α : Type u_11} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommSemiring R]
  [inst_3 : Semiring α] [inst_4 : Algebra R α] (M : Matrix m m αᵐᵒᵖ),
  AlgEquiv.mopMatrix M = MulOpposite.op (M.transpose.map MulOpposite.unop)
-- Mathlib.Algebra.Homology.QuasiIso
QuasiIsoAt.quasiIso : ∀ {ι : Type u_1} {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {c : ComplexShape ι} {K L : HomologicalComplex C c} {f : K ⟶ L}
  {i : ι} {inst_2 : K.HasHomology i} {inst_3 : L.HasHomology i} [self : QuasiIsoAt f i],
  CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor C c i).map f)
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq.match_1.eq_4 : ∀ (motive : Lean.Grind.IntInterval → Lean.Grind.IntInterval → Sort u_1)
  (h_1 : (a a_1 b b_1 : ℤ) → motive (Lean.Grind.IntInterval.co a a_1) (Lean.Grind.IntInterval.co b b_1))
  (h_2 : (a b : ℤ) → motive (Lean.Grind.IntInterval.ci a) (Lean.Grind.IntInterval.ci b))
  (h_3 : (a b : ℤ) → motive (Lean.Grind.IntInterval.io a) (Lean.Grind.IntInterval.io b))
  (h_4 : Unit → motive Lean.Grind.IntInterval.ii Lean.Grind.IntInterval.ii)
  (h_5 : (x x_1 : Lean.Grind.IntInterval) → motive x x_1),
  (match Lean.Grind.IntInterval.ii, Lean.Grind.IntInterval.ii with
    | Lean.Grind.IntInterval.co a a_1, Lean.Grind.IntInterval.co b b_1 => h_1 a a_1 b b_1
    | Lean.Grind.IntInterval.ci a, Lean.Grind.IntInterval.ci b => h_2 a b
    | Lean.Grind.IntInterval.io a, Lean.Grind.IntInterval.io b => h_3 a b
    | Lean.Grind.IntInterval.ii, Lean.Grind.IntInterval.ii => h_4 ()
    | x, x_1 => h_5 x x_1) =
    h_4 ()
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.isoTriangleOfIso₁₃_hom_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C) (hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (e₁ : T₁.obj₁ ≅ T₂.obj₁) (e₃ : T₁.obj₃ ≅ T₂.obj₃)
  (comm :
    CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map e₁.hom) =
      CategoryTheory.CategoryStruct.comp e₃.hom T₂.mor₃),
  (CategoryTheory.Pretriangulated.isoTriangleOfIso₁₃ T₁ T₂ hT₁ hT₂ e₁ e₃ comm).hom.hom₁ = e₁.hom
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopy.transReflReparamAux_zero : Path.Homotopy.transReflReparamAux 0 = 0
-- Std.Data.TreeMap.Iterator
/-- Returns a finite iterator over the values of a tree map.
The iterator yields the values in order and then terminates.

The key and value types must live in the same universe.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.TreeMap.valuesIter : {α β : Type u} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → Std.Iter β
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- The `weightedVSub` for an empty set is 0.  -/
Finset.weightedVSub_empty : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (w : ι → k) (p : ι → P), (∅.weightedVSub p) w = 0
-- Mathlib.Geometry.Euclidean.SignedDist
Affine.Simplex.signedInfDist_affineCombination : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1))
  {w : Fin (n + 1) → ℝ},
  ∑ i, w i = 1 →
    (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) =
      w i * ‖s.points i -ᵥ ↑((s.faceOpposite i).orthogonalProjectionSpan (s.points i))‖
-- Init.Data.Range.Polymorphic.PRange
Std.Ric.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (upper : α), (sizeOf *...=upper) = 1 + sizeOf upper
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.hasDetOne_adjoinNegOne_iff : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_3} [inst_2 : CommRing R]
  {𝒢 : Subgroup (GL n R)}, Even (Fintype.card n) → (𝒢.adjoinNegOne.HasDetOne ↔ 𝒢.HasDetOne)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_C_mul_X_sub_C_of_IsUnit : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (b : R) (a : Rˣ),
  (Polynomial.C ↑a * Polynomial.X - Polynomial.C b).roots = {↑a⁻¹ * b}
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
/-- The property of reflecting coequalizers expressed in terms of coforks.  -/
CategoryTheory.Limits.isColimitOfIsColimitCoforkMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {X Y Z : C} →
            {f g : X ⟶ Y} →
              {h : Y ⟶ Z} →
                (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) →
                  [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.parallelPair f g) G] →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (G.map h) ⋯) →
                      CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ h w)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k a : α}
  [inst_1 : Inhabited (β a)] {v : β k},
  (m.insertIfNew k v).get! a = if h : (k == a) = true ∧ k ∉ m then cast ⋯ v else m.get! a
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- Construct a term of `LightProfinite` from a type endowed with the structure of a compact,
Hausdorff, totally disconnected and second countable topological space.
 -/
LightProfinite.of : (X : Type u_1) →
  [inst : TopologicalSpace X] →
    [CompactSpace X] → [T2Space X] → [TotallyDisconnectedSpace X] → [SecondCountableTopology X] → LightProfinite
-- Mathlib.Analysis.Convex.Intrinsic
/-- **Alias** of `intrinsicClosure_sdiff_intrinsicFrontier`. -/
intrinsicClosure_diff_intrinsicFrontier : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (s : Set P),
  intrinsicClosure 𝕜 s \ intrinsicFrontier 𝕜 s = intrinsicInterior 𝕜 s
-- Mathlib.Order.Filter.Basic
Filter.frequently_imp_distrib : ∀ {α : Type u} {f : Filter α} {p q : α → Prop},
  (∃ᶠ (x : α) in f, p x → q x) ↔ (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in f, q x
-- Mathlib.Order.Hom.Set
Set.sumEquiv_apply : ∀ {α : Type u_1} {β : Type u_2} (s : Set (α ⊕ β)), Set.sumEquiv s = (Sum.inl ⁻¹' s, Sum.inr ⁻¹' s)
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeft_add_distrib : ∀ {w : ℕ} {x y : BitVec w} {n : ℕ}, (x + y) <<< n = x <<< n + y <<< n
-- Std.Data.DHashMap.RawLemmas
/-- Simpler variant of `getD_filter` when `LawfulBEq` is available.  -/
Std.DHashMap.Raw.Const.getD_filter' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulBEq α]
  {f : α → β → Bool} {k : α} {fallback : β},
  m.WF →
    Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.filter f m) k fallback =
      (Option.filter (f k) (Std.DHashMap.Raw.Const.get? m k)).getD fallback
-- Mathlib.LinearAlgebra.RootSystem.BaseChange
RootPairing.restrictScalars_toLinearMap_apply_apply : ∀ {ι : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field L] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module L M] [inst_4 : Module L N] (P : RootPairing ι L M N) (K : Type u_5)
  [inst_5 : Field K] [inst_6 : Algebra K L] [inst_7 : Module K M] [inst_8 : Module K N] [inst_9 : IsScalarTower K L M]
  [inst_10 : IsScalarTower K L N] [inst_11 : P.IsBalanced] [inst_12 : P.IsValuedIn K]
  (x : ↥(Submodule.span K (Set.range ⇑P.root))) (y : ↥(Submodule.span K (Set.range ⇑P.coroot))),
  (algebraMap K L) (((P.restrictScalars' K).toLinearMap x) y) = (P.toLinearMap ↑x) ↑y
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_ofNat : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) [inst_1 : n.AtLeastTwo], (OfNat.ofNat n).toFinsupp = OfNat.ofNat n
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.δ_comp_δ' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j),
  CategoryTheory.CategoryStruct.comp (X.δ i) (X.δ j) =
    CategoryTheory.CategoryStruct.comp (X.δ (j.pred ⋯)) (X.δ i.castSucc)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p q q' : ℤ) (hpq : p + n = q)
  (hq' : q' = q) {Z : C} (h : G.X q' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (γ.v p q hpq)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq G hq').inv h) =
    CategoryTheory.CategoryStruct.comp (γ.v p q' ⋯) h
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Suppose `I` is an ideal of `R`, then `R / I` is the localization away from `r : R`
if `r - 1 ∈ I` and for some `n`, `r ^ n • I = ⊥`.
For sake of usability, we state this for surjective ring maps instead of ideals.
For a version with two ideals, see `Away.of_sub_one_mem_ker'`.  -/
IsLocalization.Away.of_surjective : ∀ {S : Type u_4} {T : Type u_5} [inst : CommRing S] [inst_1 : CommRing T] [inst_2 : Algebra S T],
  Function.Surjective ⇑(algebraMap S T) →
    ∀ {r : S},
      IsUnit ((algebraMap S T) r) → ∀ (n : ℕ), r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥ → IsLocalization.Away r T
-- Aesop.Forward.State
/-- Remove the pattern substitution `subst` from `slot` and all later slots.  -/
Aesop.VariableMap.erasePatSubst : Aesop.VariableMap → Aesop.Substitution → Aesop.SlotIndex → Aesop.VariableMap
-- Mathlib.NumberTheory.WellApproximable
/-- In a seminormed additive group `A`, given `n : ℕ` and `δ : ℝ`,
`approxAddOrderOf A n δ` is the set of elements within a distance `δ` of a point of order `n`.  -/
approxAddOrderOf : (A : Type u_1) → [SeminormedAddGroup A] → ℕ → ℝ → Set A
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
/-- The function `klFun` is nonnegative on `[0,∞)`.  -/
InformationTheory.klFun_nonneg : ∀ {x : ℝ}, 0 ≤ x → 0 ≤ InformationTheory.klFun x