mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.ι_range_map_reverse : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M),
  Submodule.map CliffordAlgebra.reverse (CliffordAlgebra.ι Q).range = (CliffordAlgebra.ι Q).range
-- Mathlib.Topology.EMetricSpace.Basic
instEMetricSpaceSeparationQuotient : {X : Type u_1} → [inst : PseudoEMetricSpace X] → EMetricSpace (SeparationQuotient X)
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.mulMap_toLinearMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (A B : Subalgebra R S), (A.mulMap B).toLinearMap = (Subalgebra.toSubmodule A).mulMap (Subalgebra.toSubmodule B)
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyD : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → α → α → α
-- Mathlib.Logic.Function.Defs
Function.prod_snd_fst : ∀ {α : Type u_1} {β : Type u_2}, Function.prod Prod.snd Prod.fst = Prod.swap
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryGE?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getEntryGE? k = t₂.getEntryGE? k
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.instNonemptyConstPromiseVal : Nonempty Lean.Environment.ConstPromiseVal✝
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_congr_set : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X}, s =ᵐ[μ] t → ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in t, f x ∂μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.keysArray_filter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  {f : α → β → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.keysArray =
    (Array.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯))
        t.keysArray.attach).unattach
-- Mathlib.LinearAlgebra.Finsupp.SumProd
/-- On a `Fintype η`, `Finsupp.split` is a linear equivalence between
`(Σ (j : η), ιs j) →₀ M` and `(j : η) → (ιs j →₀ M)`.

This is the `LinearEquiv` version of `Finsupp.sigmaFinsuppAddEquivPiFinsupp`.  -/
Finsupp.sigmaFinsuppLEquivPiFinsupp : (R : Type u_5) →
  [inst : Semiring R] →
    {η : Type u_7} →
      [Fintype η] →
        {M : Type u_9} →
          {ιs : η → Type u_10} →
            [inst_2 : AddCommMonoid M] → [inst_3 : Module R M] → ((j : η) × ιs j →₀ M) ≃ₗ[R] (j : η) → ιs j →₀ M
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.all : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → (α → Bool) → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- Given `IsStrictSegal X`, a choice of inverse to `spine X n` for all `n : ℕ`
determines an inhabitant of `StrictSegal X`.  -/
SSet.StrictSegal.ofIsStrictSegal : (X : SSet) → [X.IsStrictSegal] → X.StrictSegal
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- A rewrite lemma for `padicValRat p (q^k)`.  -/
padicValRat.pow : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ) {k : ℕ}, padicValRat p (q ^ k) = ↑k * padicValRat p q
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.Subarray.Internal.toList_iter : ∀ {α : Type u} {s : Subarray α},
  (Std.Slice.Internal.iter s).toList = List.drop s.start (List.take s.stop s.array.toList)
-- Mathlib.Topology.Connected.PathConnected
/-- The map `X → ZerothHomotopy X`.  -/
ZerothHomotopy.mk : {X : Type u_1} → [inst : TopologicalSpace X] → X → ZerothHomotopy X
-- Init.Data.Range.Polymorphic.UInt
UInt64.instHasSize : Std.Rxc.HasSize UInt64
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.funSplitAt_symm_apply : ∀ (Y : Type u_2) [inst : TopologicalSpace Y] {ι : Type u_7} [inst_1 : DecidableEq ι] (i : ι)
  (f : (fun a => Y) i × ((j : { j // j ≠ i }) → (fun a => Y) ↑j)) (j : ι),
  (Homeomorph.funSplitAt Y i).symm f j = if h : j = i then f.1 else f.2 ⟨j, ⋯⟩
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_pos_of_pos_of_le_one : ∀ {x : ℝ}, 0 < x → x ≤ 1 → 0 < Real.sin x
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.t'_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i j k : D.J),
  CategoryTheory.CategoryStruct.comp (D.t' i j k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (D.f j k) (D.f j i)).hom
        (CategoryTheory.CategoryStruct.comp (D.t' j i k)
          (CategoryTheory.Limits.pullbackSymmetry (D.f i k) (D.f i j)).hom)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (D.f i j) (D.f i k))
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.OplaxTrans F G) (a : B),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a))
      (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).hom
        (CategoryTheory.Bicategory.rightUnitor (self.app a)).inv)
-- Mathlib.Algebra.Order.Floor.Ring
/-- Extension for the `positivity` tactic: `Int.fract` is always nonnegative.  -/
Mathlib.Meta.Positivity.evalIntFract : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Tactic.SetNotationForOrder
/-- Linter for ambiguous use of subset notation notation.  -/
_private.Mathlib.Tactic.SetNotationForOrder.0.Mathlib.Meta.SetNotationForOrder.linter.setNotationForOrder : Lean.Option Bool
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.fhom.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b),
  Algebra.Generators.PresentationOfFreeCotangent.Aux.fhom✝ D = { val := fun i => MvPolynomial.X i, aeval_val := ⋯ }
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.eigenspace_le_maxGenEigenspace : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R}, f.eigenspace μ ≤ f.maxGenEigenspace μ
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
AddSubgroup.addSubgroupOfContinuousAddEquivOfLe_toAddEquiv : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {H K : AddSubgroup G} (hHK : H ≤ K),
  ↑(AddSubgroup.addSubgroupOfContinuousAddEquivOfLe hHK) = AddSubgroup.addSubgroupOfEquivOfLe hHK
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldl_eq_foldl_keysArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {f : δ → α → δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldl (fun d a x => f d a) init t = Array.foldl f init t.keysArray
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeAction.mk.sizeOf_spec : ∀ (toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams) (toPartialResultParams : Lean.Lsp.PartialResultParams)
  (title : String) (kind? : Option Lean.Lsp.CodeActionKind) (diagnostics? : Option (Array Lean.Lsp.Diagnostic))
  (isPreferred? : Option Bool) (disabled? : Option Lean.Lsp.CodeActionDisabled) (edit? : Option Lean.Lsp.WorkspaceEdit)
  (command? : Option Lean.Lsp.Command) (data? : Option Lean.Json),
  sizeOf
      { toWorkDoneProgressParams := toWorkDoneProgressParams, toPartialResultParams := toPartialResultParams,
        title := title, kind? := kind?, diagnostics? := diagnostics?, isPreferred? := isPreferred?,
        disabled? := disabled?, edit? := edit?, command? := command?, data? := data? } =
    1 + sizeOf toWorkDoneProgressParams + sizeOf toPartialResultParams + sizeOf title + sizeOf kind? +
                sizeOf diagnostics? +
              sizeOf isPreferred? +
            sizeOf disabled? +
          sizeOf edit? +
        sizeOf command? +
      sizeOf data?
-- Mathlib.Order.RelIso.Basic
RelHom.coe_fn_toFun : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s), f.toFun = ⇑f
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_integrable : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  (f : MeasureTheory.SimpleFunc α E), MeasureTheory.Integrable (⇑f) μ → ∀ {x : E}, x ≠ 0 → μ (⇑f ⁻¹' {x}) < ⊤
-- Lean.PrettyPrinter.Delaborator.Basic
/-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options.  -/
Lean.PrettyPrinter.delab : Lean.Expr → optParam Lean.PrettyPrinter.Delaborator.OptionsPerPos ∅ → Lean.MetaM Lean.Term
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.isSymm_toBilin_iff_isSymm : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁) {M : Matrix n n R₁},
  ((Matrix.toBilin b) M).IsSymm ↔ M.IsSymm
-- Mathlib.Topology.Algebra.Ring.Ideal
QuotientRing.isOpenQuotientMap_mk : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommRing R] (N : Ideal R) [IsTopologicalRing R],
  IsOpenQuotientMap ⇑(Ideal.Quotient.mk N)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k a : α} {v : β k} {h₁ : a ∈ t.insert k v},
  (t.insert k v).getKey a h₁ = if h₂ : cmp k a = Ordering.eq then k else t.getKey a ⋯
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
/-- The complete integral closure is the subalgebra of almost integral elements.  -/
completeIntegralClosure : (R : Type u_1) → (S : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Subalgebra R S
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeLeftOpOfConeEquiv_unitIso : ∀ {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.Limits.coconeLeftOpOfConeEquiv.unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)ᵒᵖ)
-- Init.Data.Array.Lemmas
Array.mem_of_mem_push_of_mem : ∀ {α : Type u_1} {a b : α} {xs : Array α}, a ∈ xs.push b → b ∈ xs → a ∈ xs
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- A general form of Möbius inversion. Based on lemma 2.1.2 of Incidence Algebras by Spiegel and
O'Donnell.  -/
IncidenceAlgebra.moebius_inversion_top : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Ring 𝕜] [inst_1 : PartialOrder α] [inst_2 : OrderTop α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] (f g : α → 𝕜),
  (∀ (x : α), g x = ∑ y ≥ x, f y) → ∀ (x : α), f x = ∑ y ≥ x, (IncidenceAlgebra.mu 𝕜) x y * g y
-- Mathlib.Algebra.Star.Pointwise
Set.instInvolutiveStar.eq_1 : ∀ {α : Type u_1} [inst : InvolutiveStar α], Set.instInvolutiveStar = { toStar := Set.star, star_involutive := ⋯ }
-- Mathlib.Geometry.RingedSpace.Basic
/-- If a section `f` is a unit in each stalk, `f` must be a unit.  -/
AlgebraicGeometry.RingedSpace.isUnit_of_isUnit_germ : ∀ (X : AlgebraicGeometry.RingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace)
  (f : ↑(X.presheaf.obj (Opposite.op U))),
  (∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U),
      IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) f)) →
    IsUnit f
-- Mathlib.Combinatorics.Graph.Delete
Graph.restrict_inter_edgeSet : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β), G.restrict (F ∩ G.edgeSet) = G.restrict F
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.notMem₁ : ∀ {X : SSet} {A : X.Subcomplex} (self : A.PairingCore) (s : self.ι),
  self.simplex s ∉ A.obj (Opposite.op { len := self.dim s + 1 })
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.RigidCategory.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [toRightRigidCategory : CategoryTheory.RightRigidCategory C] →
        [toLeftRigidCategory : CategoryTheory.LeftRigidCategory C] → CategoryTheory.RigidCategory C
-- Mathlib.Topology.ContinuousMap.LocallyConstant
LocallyConstant.separatesPoints_range_toContinuousMapAlgHom : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (R : Type u_3)
  [inst_2 : CommSemiring R] [TotallySeparatedSpace X] [inst_4 : Semiring Y] [inst_5 : Algebra R Y]
  [inst_6 : IsTopologicalSemiring Y] [Nontrivial Y], (LocallyConstant.toContinuousMapAlgHom R).range.SeparatesPoints
-- Mathlib.Order.Filter.EventuallyConst
Filter.eventuallyConst_set : ∀ {α : Type u_1} {l : Filter α} {s : Set α},
  Filter.EventuallyConst s l ↔ (∀ᶠ (x : α) in l, x ∈ s) ∨ ∀ᶠ (x : α) in l, x ∉ s
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.Hom.generate_singleton_mem_propQCTopology : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  P f →
    ∀ [AlgebraicGeometry.Surjective f] [AlgebraicGeometry.QuasiCompact f],
      CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton f) ∈
        (AlgebraicGeometry.Scheme.propQCTopology P) Y
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftHom.whiskerRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : Mathlib.Tactic.Coherence.LiftObj X] →
            [inst_3 : Mathlib.Tactic.Coherence.LiftObj Y] →
              [Mathlib.Tactic.Coherence.LiftHom f] →
                {Z : C} →
                  [inst_5 : Mathlib.Tactic.Coherence.LiftObj Z] →
                    Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.mul.sizeOf_spec : sizeOf Std.Tactic.BVDecide.BVBinOp.mul = 1
-- Mathlib.Data.Nat.Factorial.SuperFactorial
_private.Mathlib.Data.Nat.Factorial.SuperFactorial.0.Nat.superFactorial.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Algebra.LinearRecurrence
LinearRecurrence.mk : {R : Type u_1} → [inst : CommSemiring R] → (order : ℕ) → (Fin order → R) → LinearRecurrence R
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ∀ (f : α → ENNReal) (t : Set α), ∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in t ∩ (g +ᵥ s), f x ∂μ
-- Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
/-- The product of almost everywhere strongly measurable functions is measurable.  -/
MeasureTheory.AEStronglyMeasurable.tprod : ∀ {X : Type u_4} {E : Type u_5} {ι : Type u_6} [inst : MeasurableSpace X] [inst_1 : CommMonoid E]
  [inst_2 : TopologicalSpace E] [ContinuousMul E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace E] [Countable ι] {μ : MeasureTheory.Measure X} {f : ι → X → E},
  (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) →
    MeasureTheory.AEStronglyMeasurable (fun x => ∏'[L] (i : ι), f i x) μ
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.instNoPrefixPatternModelChar : ∀ {c : Char}, String.Slice.Pattern.Model.NoPrefixPatternModel c
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.powerBasisAux.eq_1 : ∀ {K : Type u_5} [inst : Field K] {f : Polynomial K} (hf : f ≠ 0), AdjoinRoot.powerBasisAux hf = Module.Basis.mk ⋯ ⋯
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.pseudofunctor_toPrelaxFunctor : CategoryTheory.WithTerminal.pseudofunctor.toPrelaxFunctor = CategoryTheory.WithTerminal.prelaxfunctor
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_le_ringKrullDim_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} [I.IsPrime], ↑I.height ≤ ringKrullDim R
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.aeval_coe : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {a : S} [inst_2 : UniformSpace R]
  [inst_3 : UniformSpace S] [inst_4 : IsUniformAddGroup R] [inst_5 : IsTopologicalSemiring R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : T2Space S] [inst_8 : CompleteSpace S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S] (ha : PowerSeries.HasEval a)
  (p : Polynomial R), (PowerSeries.aeval ha) ↑p = (Polynomial.aeval a) p
-- Mathlib.Algebra.Lie.Prod
LieHom.prodMap_id : ∀ {R : Type u_1} {L₁ : Type u_2} {L : Type u_4} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L], LieHom.id.prodMap LieHom.id = LieHom.id
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
/-- **Alias** of `CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_hom`. -/
CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : CategoryTheory.CartesianMonoidalCategory A]
  {X W : CategoryTheory.Sheaf J A} (f : W ⟶ X),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.obj f.hom
-- Mathlib.Analysis.Real.OfDigits
Real.ofDigits_digits : ∀ {b : ℕ} [inst : NeZero b] {x : ℝ}, 1 < b → x ∈ Set.Ico 0 1 → Real.ofDigits (x.digits b) = x
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- The second generator of an intermediate field of the form `K⟮x, y⟯`.  -/
IntermediateField.AdjoinPair.gen₂ : (K : Type u_1) → {L : Type u_2} → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → (x y : L) → ↥K⟮x, y⟯
-- Mathlib.Analysis.Convex.Visible
isVisible_comm : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsOrderedRing 𝕜]
  [inst_3 : AddCommGroup V] [inst_4 : Module 𝕜 V] [inst_5 : AddTorsor V P] {s : Set P} {x y : P},
  IsVisible 𝕜 s x y ↔ IsVisible 𝕜 s y x
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
AlgebraicGeometry.SurjectiveOnStalks.instHasRingHomPropertySurjectiveOnStalks : AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.SurjectiveOnStalks fun {R S} [CommRing R] [CommRing S] =>
  RingHom.SurjectiveOnStalks
-- Mathlib.Algebra.Polynomial.Degree.Units
Polynomial.degree_coe_units : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] [Nontrivial R] (u : (Polynomial R)ˣ), (↑u).degree = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_filter_not_contains_map_fst_of_containsKey_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getKey? k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) = none
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
RightPreLieAlgebra.ext_iff : ∀ {R : Type u_1} {inst : CommRing R} {L : Type u_2} {inst_1 : RightPreLieRing L} {x y : RightPreLieAlgebra R L},
  x = y ↔ SMul.smul = SMul.smul
-- Mathlib.Topology.Category.TopCat.EffectiveEpi
/-- Implementation: If `π` is a morphism in `TopCat` which is a quotient map, then it is an effective
epimorphism. The theorem `TopCat.effectiveEpi_iff_isQuotientMap` should be used instead of
this definition.
 -/
TopCat.effectiveEpiStructOfQuotientMap : {B X : TopCat} →
  (π : X ⟶ B) → Topology.IsQuotientMap ⇑(CategoryTheory.ConcreteCategory.hom π) → CategoryTheory.EffectiveEpiStruct π
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.ι_injective : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] [Nontrivial R], Function.Injective (FreeAlgebra.ι R)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
tangentMapWithin_subset : ∀ {𝕜 : 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'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s t : Set M}
  {p : TangentBundle I M},
  s ⊆ t → UniqueMDiffAt[s] p.proj → MDiffAt[t] f p.proj → tangentMapWithin I I' f s p = tangentMapWithin I I' f t p
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.comapDomain_apply : ∀ {ι : Type u} {β : ι → Type v} {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : κ → ι) (hh : Function.Injective h)
  (f : Π₀ (i : ι), β i) (k : κ), (DFinsupp.comapDomain h hh f) k = f (h k)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toRingHom_comp_symm_toRingHom : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (e : R ≃+* S),
  e.toRingHom.comp e.symm.toRingHom = RingHom.id S
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coequalizerComparison_map_desc_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] {Z : C} {h : Y ⟶ Z}
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) {Z_1 : D} (h_1 : G.obj Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizerComparison f g G)
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.desc h w)) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.desc (G.map h) ⋯) h_1
-- Mathlib.Algebra.Lie.Derivation.Killing
/-- The restriction of the Killing form of a finite-dimensional Killing Lie algebra to the range of
the adjoint action is nondegenerate.  -/
LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate : ∀ (R : Type u_1) (L : Type u_2) [inst : Field R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [Module.Finite R L]
  [LieAlgebra.IsKilling R L],
  ((killingForm R (LieDerivation R L L)).restrict (LieDerivation.ad R L).range.toSubmodule).Nondegenerate