mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.CharP.Algebra
/-- If `R →+* A` is injective, and `A` is of characteristic `p`, then `R` is also of
characteristic `p`. Similar to `RingHom.charZero`.  -/
RingHom.charP : ∀ {R : Type u_1} {A : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring A] (f : R →+* A),
  Function.Injective ⇑f → ∀ (p : ℕ) [CharP A p], CharP R p
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.pairing_apply : ∀ {𝕜 : Type u_2} {D : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedAddCommGroup D]
  [inst_7 : NormedSpace ℝ D] [inst_8 : NormedAddCommGroup G] [inst_9 : NormedSpace ℝ G] [inst_10 : NormedSpace 𝕜 F]
  [inst_11 : NormedSpace 𝕜 E] [inst_12 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) (f : SchwartzMap D E)
  (g : SchwartzMap D F), ⇑(((SchwartzMap.pairing B) f) g) = fun x => (B (f x)) (g x)
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso_eq : ∀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'}
  {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₁ hF).unitIso =
    AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso hF
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
CategoryTheory.Square.IsPullback.map_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F]
  [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F],
  (sq.map F).IsPullback ↔ sq.IsPullback
-- Mathlib.Algebra.Star.Basic
StarMemClass.instStar : {R : Type u} → {S : Type w} → [inst : Star R] → [inst_1 : SetLike S R] → [hS : StarMemClass S R] → (s : S) → Star ↥s
-- Init.GetElem
getElem!_neg : ∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [inst : GetElem? cont idx elem dom]
  [LawfulGetElem cont idx elem dom] [inst_2 : Inhabited elem] (c : cont) (i : idx), ¬dom c i → c[i]! = default
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_funUnique_symm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Unique ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : TopologicalSpace M], ⇑(ContinuousLinearEquiv.funUnique ι R M).symm = Function.const ι
-- 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) [inst_2 : Nonempty (↑s → F → ↑(proj ⁻¹' s))] (z : ↑(proj ⁻¹' s)),
  ↑(e.restrictPreimage' s).toPartialEquiv z = (⟨proj ↑z, ⋯⟩, (↑e ↑z).2)
-- Mathlib.RingTheory.Valuation.Integers
Valuation.integer.integers : ∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀),
  v.Integers ↥v.integer
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- If `f : ℝ → ℝ` is strictly positive everywhere, and integrable on `(a, b]` for real numbers
`a < b`, then its integral over `a..b` is strictly positive. (See `intervalIntegral_pos_of_pos_on`
for a version only assuming positivity of `f` on `(a, b)` rather than everywhere.)  -/
intervalIntegral.intervalIntegral_pos_of_pos : ∀ {f : ℝ → ℝ} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b → (∀ (x : ℝ), 0 < f x) → a < b → 0 < ∫ (x : ℝ) in a..b, f x
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
spectrum.exists_mem_of_not_isUnit_aeval_prod : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [inst_3 : IsDomain R]
  {p : Polynomial R} {a : A},
  ¬IsUnit ((Polynomial.aeval a) (Multiset.map (fun x => Polynomial.X - Polynomial.C x) p.roots).prod) →
    ∃ k ∈ spectrum R a, Polynomial.eval k p = 0
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.hadamard_one_eq_diagonal_iff : ∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : MulZeroOneClass α] {A : Matrix n n α} {d : n → α},
  A.hadamard 1 = Matrix.diagonal d ↔ A.diag = d
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
/-- The image of a topologically nilpotent element under a continuous morphism
is topologically nilpotent  -/
IsTopologicallyNilpotent.map : ∀ {R : Type u_1} {S : Type u_2} [inst : TopologicalSpace R] [inst_1 : MonoidWithZero R] [inst_2 : MonoidWithZero S]
  [inst_3 : TopologicalSpace S] {F : Type u_3} [inst_4 : FunLike F R S] [MonoidWithZeroHomClass F R S] {φ : F},
  Continuous ⇑φ → ∀ {a : R}, IsTopologicallyNilpotent a → IsTopologicallyNilpotent (φ a)
-- Mathlib.Data.Matrix.Basic
/-- The `Equiv` between spaces of matrices induced by an `Equiv` between their
coefficients. This is `Matrix.map` as an `Equiv`.  -/
Equiv.mapMatrix : {m : Type u_2} → {n : Type u_3} → {α : Type u_11} → {β : Type u_12} → α ≃ β → Matrix m n α ≃ Matrix m n β
-- Mathlib.Topology.Order
induced_generateFrom_eq : ∀ {α : Type u_1} {β : Type u_2} {b : Set (Set β)} {f : α → β},
  TopologicalSpace.induced f (TopologicalSpace.generateFrom b) = TopologicalSpace.generateFrom (Set.preimage f '' b)
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Combine a family of covers over a cover.  -/
CategoryTheory.GrothendieckTopology.Cover.bind : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} → {X : C} → (S : J.Cover X) → ((I : S.Arrow) → J.Cover I.Y) → J.Cover X
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.Indep.isBasis_of_eRk_ge : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  M.Indep I →
    I.Finite → I ⊆ X → M.eRk X ≤ M.eRk I → autoParam (X ⊆ M.E) Matroid.Indep.isBasis_of_eRk_ge._auto_1 → M.IsBasis I X
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.forward.eq_def : ∀ (x : String.Legacy.Iterator) (x_1 : ℕ),
  x.forward x_1 =
    match x, x_1 with
    | it, 0 => it
    | it, n.succ => it.next.forward n
-- Mathlib.ModelTheory.Definability
Set.DefinableFun.mono : ∀ {M : Type u_1} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u_2} {A : Set M} {f : (α → M) → M}
  {B : Set M}, Set.DefinableFun L A f → A ⊆ B → Set.DefinableFun L B f
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_apply : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (f : α → ℝ)
  (s : Set α), (μ.tilted f) s = ∫⁻ (a : α) in s, ENNReal.ofReal (Real.exp (f a) / ∫ (x : α), Real.exp (f x) ∂μ) ∂μ
-- Mathlib.Data.Set.UnionLift
/-- Given a union of sets `iUnion S`, define a function on the Union by defining
it on each component, and proving that it agrees on the intersections.  -/
Set.iUnionLift : {α : Type u_1} →
  {ι : Sort u_2} →
    {β : Sort u_3} →
      (S : ι → Set α) →
        (f : (i : ι) → ↑(S i) → β) →
          (∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩) →
            (T : Set α) → T ⊆ Set.iUnion S → ↑T → β
-- Mathlib.Computability.NFA
/-- `M.stepSet S a` is the union of `M.step s a` for all `s ∈ S`.  -/
NFA.stepSet : {α : Type u} → {σ : Type v} → NFA α σ → Set σ → α → Set σ
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.IsStandardSmooth.exists_etale_mvPolynomial : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.IsStandardSmooth → ∃ n g, g.comp MvPolynomial.C = f ∧ g.Etale
-- Init.System.Uri
System.Uri.UriEscape.nine : UInt8
-- Mathlib.RingTheory.IsAdjoinRoot
/-- Transfer `IsAdjoinRoot` across an algebra isomorphism.

This is the converse of `IsAdjoinRoot.algEquiv`: this turns an `AlgEquiv` into an `IsAdjoinRoot`,
and `IsAdjoinRoot.algEquiv` turns an `IsAdjoinRoot` into an `AlgEquiv`.
 -/
IsAdjoinRoot.ofAlgEquiv : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : Ring S] →
        {f : Polynomial R} →
          [inst_2 : Algebra R S] →
            IsAdjoinRoot S f →
              {T : Type u_1} → [inst_3 : Ring T] → [inst_4 : Algebra R T] → (S ≃ₐ[R] T) → IsAdjoinRoot T f
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.coev_app_comp_pre_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A B : C} (X : C)
  [inst_2 : CategoryTheory.Closed A] [inst_3 : CategoryTheory.Closed B] (f : B ⟶ A),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app X)
      ((CategoryTheory.MonoidalClosed.pre f).app (CategoryTheory.MonoidalCategoryStruct.tensorObj A X)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev B).app X)
      ((CategoryTheory.ihom B).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Spec.map_preimage_unop : ∀ {R S : CommRingCat} (f : AlgebraicGeometry.Spec R ⟶ AlgebraicGeometry.Spec S),
  AlgebraicGeometry.Spec.map (AlgebraicGeometry.Spec.fullyFaithful.preimage f).unop = f
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.checkLowerHex : ℕ → (s : String) → s.Pos → Bool
-- Mathlib.Order.SymmDiff
bihimp_himp_eq_inf : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), bihimp a (a ⇨ b) = a ⊓ b
-- Std.Http.Data.URI.Basic
/-- Complete URI structure following RFC 3986. All text components use encoded string types to ensure
proper percent-encoding.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html
 -/
Std.Http.URI : Type
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.centralizer_eq_top_iff_subset : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] {s : Set R},
  NonUnitalSubsemiring.centralizer s = ⊤ ↔ s ⊆ ↑(NonUnitalSubsemiring.center R)
-- Mathlib.Algebra.DirectSum.Module
DirectSum.linearEquivFunOnFintype_symm_coe : ∀ (R : Type u) [inst : Semiring R] (ι : Type v) (M : ι → Type w) [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Fintype ι] (f : DirectSum ι fun i => M i),
  (DirectSum.linearEquivFunOnFintype R ι M).symm ⇑f = f
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Module.lift_apply : ∀ (R : Type u_1) (ι : Type u_2) [inst : Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Semiring R]
  [inst_5 : (i : ι) → AddCommMonoid (G i)] [inst_6 : (i : ι) → Module R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] {P : Type u_7}
  [inst_9 : AddCommMonoid P] [inst_10 : Module R P] (g : (i : ι) → G i →ₗ[R] P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (z : DirectLimit G f),
  (DirectLimit.Module.lift R ι G f g Hg) z = DirectLimit.lift f (fun x1 x2 => (g x1) x2) ⋯ z
-- Mathlib.RepresentationTheory.Invariants
Representation.linHom.invariantsEquivRepHom_symm_apply_coe : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (X Y : Rep.{w, u, v} k G) (f : X ⟶ Y),
  ↑((Representation.linHom.invariantsEquivRepHom X Y).symm f) = ↑(Rep.Hom.hom f)
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.map.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K K' : ChainComplex C ℕ} {L L' : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L)
  (h' : CochainComplex.ConnectData K' L') (fK fK_1 : K ⟶ K') (e_fK : fK = fK_1) (fL fL_1 : L ⟶ L') (e_fL : fL = fL_1)
  (f_comm : CategoryTheory.CategoryStruct.comp (fK.f 0) h'.d₀ = CategoryTheory.CategoryStruct.comp h.d₀ (fL.f 0)),
  h.map h' fK fL f_comm = h.map h' fK_1 fL_1 ⋯
-- Std.Data.TreeSet.Basic
Std.TreeSet.instEmptyCollection : {α : Type u} → {cmp : α → α → Ordering} → EmptyCollection (Std.TreeSet α cmp)
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.pfilter.match_1.eq_2 : ∀ {α : Type u_1} (motive : (o : Option α) → ((a : α) → o = some a → Bool) → Sort u_2) (a : α)
  (p : (a_1 : α) → some a = some a_1 → Bool) (h_1 : (p : (a : α) → none = some a → Bool) → motive none p)
  (h_2 : (a : α) → (p : (a_1 : α) → some a = some a_1 → Bool) → motive (some a) p),
  (match some a, p with
    | none, p => h_1 p
    | some a, p => h_2 a p) =
    h_2 a p
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.singleAddHom_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R),
  (MonoidAlgebra.singleAddHom m) r = MonoidAlgebra.single m r
-- Mathlib.SetTheory.Cardinal.Aleph
/-- Initial ordinals are order-isomorphic to the cardinals.  -/
Ordinal.isInitialIso : { x // x.IsInitial } ≃o Cardinal.{u_1}
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLE?.go.eq_2 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (best : Option (α × β)) (size : ℕ) (k' : α) (v' : β)
  (l r : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.getEntryLE?.go k best (Std.DTreeMap.Internal.Impl.inner size k' v' l r) =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.getEntryLE?.go k best l
    | Ordering.eq => some (k', v')
    | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.getEntryLE?.go k (some (k', v')) r
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono_attachCells_isColimit₂ : ∀ {X Y : SSet} (i : X ⟶ Y) [inst : CategoryTheory.Mono i] (d : ℕ) (x : ¬IsMax d),
  ((SSet.relativeCellComplexOfMono i).attachCells d x).isColimit₂ =
    CategoryTheory.Limits.coproductIsCoproduct fun i => SSet.stdSimplex.obj { len := d }
-- Mathlib.Algebra.Category.BoolRing
boolRingCatEquivBoolAlg_functor : boolRingCatEquivBoolAlg.functor = CategoryTheory.forget₂ BoolRing BoolAlg
-- Mathlib.Data.PNat.Basic
Nat.succPNat_injective : Function.Injective Nat.succPNat
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
_private.Mathlib.RingTheory.Extension.Cotangent.BaseChange.0.Algebra.Extension.tensorCotangentSpace.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S) (T : Type u_4) [inst_3 : CommRing T] [inst_4 : Algebra R T],
  P.tensorCotangentSpace T =
    ((IsTensorProduct.assocOfMapSMul (TensorProduct.mk R T S) ⋯ (TensorProduct.mk P.Ring S Ω[P.Ring⁄R]) ⋯ ⋯
                ⋯).symm.trans
          (LinearEquiv.restrictScalars T
            (TensorProduct.AlgebraTensorModule.cancelBaseChange P.Ring P.baseChange.Ring P.baseChange.Ring
                (TensorProduct R T S) Ω[P.Ring⁄R]).symm)).trans
      (LinearEquiv.restrictScalars T
        (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.refl P.baseChange.Ring (TensorProduct R T S))
          (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring P.baseChange.Ring)))
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.pullback_obj_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (f : X ⟶ Y) (g : CategoryTheory.MonoOver Y),
  ((CategoryTheory.MonoOver.pullback f).obj g).arrow =
    CategoryTheory.Limits.pullback.snd ((CategoryTheory.MonoOver.forget Y).obj g).hom f
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- The natural transformation `shrink.{w} F ⟶ shrink.{w} G` induces by a natural
transformation `τ : F ⟶ G` between `w`-small functors to types.  -/
CategoryTheory.FunctorToTypes.shrinkMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C (Type w')} →
      (F ⟶ G) →
        [inst_1 : CategoryTheory.FunctorToTypes.Small.{w, w', v, u} F] →
          [inst_2 : CategoryTheory.FunctorToTypes.Small.{w, w', v, u} G] →
            CategoryTheory.FunctorToTypes.shrink.{w, w', v, u} F ⟶ CategoryTheory.FunctorToTypes.shrink.{w, w', v, u} G
-- Mathlib.Order.WellFoundedSet
Set.isWF_singleton : ∀ {α : Type u_2} [inst : Preorder α] {a : α}, {a}.IsWF
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.int_gcd_helper' : ∀ {d : ℕ} {x y : ℤ} (a b : ℤ), ↑d ∣ x → ↑d ∣ y → x * a + y * b = ↑d → x.gcd y = d
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.indep : ∀ (self : PeriodPair), LinearIndependent ℝ ![self.ω₁, self.ω₂]
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Qq-fied version of `Expr` proving some `P : Prop`.  -/
ExistsAndEq.HypQ : Type
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.Section.neg_add_mem_range_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  {S : AddGroupExtension N E G} (σ σ' : S.Section) (g : G), -σ g + σ' g ∈ S.inl.range
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.minKeyD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minKeyD fallback = t₂.minKeyD fallback
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.reverse_add : ∀ {α : Type u_1} {a b : FreeAddMonoid α}, (a + b).reverse = b.reverse + a.reverse
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateSubgroup.card_mul_self_le : ∀ {G : Type u_1} [inst : Group G] {K : ℝ} [inst_1 : DecidableEq G] {A : Finset G},
  IsApproximateSubgroup K ↑A → ↑(A * A).card ≤ K * ↑A.card
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Trie.node : {α : Type} →
  Array α →
    Option Lean.Meta.RefinedDiscrTree.TrieIndex →
      Std.HashMap ℕ Lean.Meta.RefinedDiscrTree.TrieIndex →
        Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex →
          Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α) → Lean.Meta.RefinedDiscrTree.Trie α
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.semigroup.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Semigroup α],
  Finset.semigroup = Function.Injective.semigroup SetLike.coe ⋯ ⋯
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- If `x : B` is integral over `R`, then it is an element of the integral closure of `R` in `B`.  -/
IsIntegralClosure.mk' : {R : Type u_1} →
  (A : Type u_2) →
    {B : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R B] → [inst_4 : Algebra A B] → [IsIntegralClosure A R B] → (x : B) → IsIntegral R x → A
-- Mathlib.CategoryTheory.Limits.Final
/-- Final functors preserve filteredness.

This can be seen as a generalization of `IsFiltered.of_right_adjoint` (which states that right
adjoints preserve filteredness), as right adjoints are always final, see `final_of_adjunction`.
 -/
CategoryTheory.IsFilteredOrEmpty.of_final : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Final] [CategoryTheory.IsFilteredOrEmpty C], CategoryTheory.IsFilteredOrEmpty D
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_monomial : ∀ {R : Type u_1} {m n : ℕ} [inst : Semiring R] {a : R}, ((SkewPolynomial.monomial n) a).coeff m = if n = m then a else 0
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.projIcc : ∀ {a b : ℝ} (h : a ≤ b), LipschitzWith 1 (Set.projIcc a b h)
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.lratChecker.match_3.congr_eq_5 : ∀ {α : Type u_1} {β : Type u_2} (motive : List (Std.Tactic.BVDecide.LRAT.Action β α) → Sort u_3)
  (prf : List (Std.Tactic.BVDecide.LRAT.Action β α)) (h_1 : Unit → motive [])
  (h_2 :
    (id : ℕ) →
      (rupHints : Array ℕ) →
        (tail : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
          motive (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail))
  (h_3 :
    (id : ℕ) →
      (c : β) →
        (rupHints : Array ℕ) →
          (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
            motive (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf))
  (h_4 :
    (id : ℕ) →
      (c : β) →
        (pivot : Std.Sat.Literal α) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                motive (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf))
  (h_5 :
    (ids : Array ℕ) →
      (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
        motive (Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf))
  (ids : Array ℕ) (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)),
  prf = Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf →
    (match prf with
      | [] => h_1 ()
      | Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail => h_2 id rupHints tail
      | Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf => h_3 id c rupHints restPrf
      | Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf =>
        h_4 id c pivot rupHints ratHints restPrf
      | Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf => h_5 ids restPrf) ≍
      h_5 ids restPrf
-- Mathlib.Analysis.Fourier.Notation
FourierTransform.fourierCLE_apply : ∀ {R : Type u_5} {E : Type u_6} {F : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : FourierTransform E F] [inst_6 : FourierAdd E F]
  [inst_7 : FourierSMul R E F] [inst_8 : FourierTransformInv F E] [inst_9 : FourierPair E F]
  [inst_10 : FourierInvPair F E] [inst_11 : TopologicalSpace E] [inst_12 : TopologicalSpace F]
  [inst_13 : ContinuousFourier E F] [inst_14 : ContinuousFourierInv F E] (f : E),
  (FourierTransform.fourierCLE R E) f = FourierTransform.fourier f
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- The `n`-th roots of unity, for `n ∈ S` nonzero, generate `B` as an `A`-algebra.  -/
IsCyclotomicExtension.adjoin_roots : ∀ {S : Set ℕ} {A : Type u} {B : Type v} {inst : CommRing A} {inst_1 : CommRing B} {inst_2 : Algebra A B}
  [self : IsCyclotomicExtension S A B] (x : B), x ∈ Algebra.adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
-- Mathlib.Data.Stream.Init
Stream'.map_append_stream : ∀ {α : Type u} {β : Type v} (f : α → β) (l : List α) (s : Stream' α),
  Stream'.map f (l ++ₛ s) = List.map f l ++ₛ Stream'.map f s
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
/-- `TensorProduct.rid` preserves tensor products of quadratic forms.  -/
QuadraticForm.tensorRId : {R : Type uR} →
  {M₁ : Type uM₁} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M₁] →
        [inst_2 : Module R M₁] →
          [inst_3 : Invertible 2] → (Q₁ : QuadraticForm R M₁) → QuadraticMap.IsometryEquiv (Q₁.tmul QuadraticMap.sq) Q₁
-- Init.Data.Range.Polymorphic.Map
/-- An injective mapping between two types implementing `UpwardEnumerable` that commutes with `succ?`
and `succMany?`.

Having such a mapping means that all of the `Prop`-valued lawfulness classes around
`UpwardEnumerable` can be pulled back.
 -/
Std.PRange.UpwardEnumerable.Map : (α : Type u) → (β : Type v) → [Std.PRange.UpwardEnumerable α] → [Std.PRange.UpwardEnumerable β] → Type (max u v)
-- Lean.Compiler.LCNF.Basic
/-- Return whether the object stored behind `fvarId` is shared or not. The return type is a `UInt8`.
 -/
Lean.Compiler.LCNF.LetValue.isShared : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_25 →
      Lean.Compiler.LCNF.LetValue pu