mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finsupp.Notation
/-- `Finsupp` elaborator for `update₀`.  -/
Finsupp.Internal.elabUpdate₀ : Lean.Elab.Term.TermElab
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.condIndepFun_finsetProd_of_notMem : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β}
  [inst_2 : CommMonoid β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.CondIndepFun m' hm' (∏ j ∈ s, f j) (f i) μ
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : Inhabited α] [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ ∪ m₂).getKey! k = m₁.getKey! k
-- Std.Do.WP.SimpLemmas
Std.Do.WP.restoreM_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε α : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (x : m (Except ε α)),
  (Std.Do.wp (MonadControl.restoreM x)).apply Q = (Std.Do.wp x).apply (fun e => Except.casesOn e Q.2.1 Q.1, Q.2.2)
-- Mathlib.Topology.UrysohnsLemma
/-- The inner set in the inductive construction towards Urysohn's lemma  -/
Urysohns.CU.C : {X : Type u_2} → [inst : TopologicalSpace X] → {P : Set X → Set X → Prop} → Urysohns.CU P → Set X
-- Mathlib.LinearAlgebra.FreeModule.Determinant
LinearMap.det_zero'' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M] [Nontrivial M], LinearMap.det 0 = 0
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.small_Ioo : ∀ (a b : Ordinal.{u}), Small.{u, u + 1} ↑(Set.Ioo a b)
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.codisjoint_subgroupOf_sup : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K))
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Expressions of the form `η ▷ f₁ ▷ ... ▷ fₙ`.  -/
Mathlib.Tactic.BicategoryLike.WhiskerRight : Type
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.toAddSubgroup_comap : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst_1 : AddGroup H] (f : G →+ H)
  (K : FiniteIndexNormalAddSubgroup H),
  (FiniteIndexNormalAddSubgroup.comap f K).toAddSubgroup = AddSubgroup.comap f K.toAddSubgroup
-- Mathlib.Topology.Spectral.ConstructibleTopology
WithConstructibleTopology.isOpen_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set (WithConstructibleTopology X)},
  IsOpen s ↔ IsOpen (WithTopology.toTopology (constructibleTopology X) ⁻¹' s)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.getValueCast? a (⟨k, v⟩ :: l) =
    if h : (k == a) = true then some (cast ⋯ v) else Std.Internal.List.getValueCast? a l
-- Mathlib.Combinatorics.HalesJewett
/-- We require combinatorial lines to be nontrivial in the sense that `fun x ↦ l x i` is `id` for
at least one coordinate `i`.  -/
Combinatorics.Line.proper : ∀ {α : Type u_5} {ι : Type u_6} (self : Combinatorics.Line α ι), ∃ i, self.idxFun i = none
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.comap_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Functor C MonCat),
  CategoryTheory.SubmonoidFunctor.comap (CategoryTheory.CategoryStruct.id M) ⊤ = ⊤
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.greatestFib_fib : ∀ {n : ℕ}, n ≠ 1 → (Nat.fib n).greatestFib = n
-- Init.Data.Nat.Lemmas
Nat.one_lt_iff_ne_zero_and_ne_one : ∀ {n : ℕ}, 1 < n ↔ n ≠ 0 ∧ n ≠ 1
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcCallParams.params : Lean.Lsp.RpcCallParams → Lean.Json
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.mapRange_add : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {N : Type u_4} [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N] [inst_4 : ContinuousAdd M]
  [inst_5 : ContinuousAdd N] {v w : MeasureTheory.VectorMeasure α M} {f : M →+ N} (hf : Continuous ⇑f),
  (v + w).mapRange f hf = v.mapRange f hf + w.mapRange f hf
-- Mathlib.Algebra.Ring.NonZeroDivisors
isLeftRegular_iff_mem_nonZeroDivisorsLeft : ∀ {R : Type u_1} [inst : Ring R] {r : R}, IsLeftRegular r ↔ r ∈ nonZeroDivisorsLeft R
-- Lean.Meta.Tactic.Acyclic
_private.Lean.Meta.Tactic.Acyclic.0.Lean.MVarId.isTarget : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addXYZ_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P Q : Fin 3 → R) (u v : R),
  W'.addXYZ (u • P) (v • Q) = (u * v) ^ 2 • W'.addXYZ P Q
-- Lean.Parser.Term
Lean.Parser.Term.nofun.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.center_re : ∀ (z : UpperHalfPlane) (r : ℝ), (z.center r).re = z.re
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.const_sub : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddCommGroup α],
  Function.Periodic f c → ∀ (a : α), Function.Periodic (fun x => f (a - x)) c
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.applyAsHom_comm : ∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : CommMonoid G] {A B : Rep.{u_1, u, v} k G} (f : A ⟶ B) (g : G),
  CategoryTheory.CategoryStruct.comp (A.applyAsHom g) f = CategoryTheory.CategoryStruct.comp f (B.applyAsHom g)
-- Mathlib.Topology.Defs.Induced
Topology.IsClosedEmbedding.mk : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
  Topology.IsEmbedding f → IsClosed (Set.range f) → Topology.IsClosedEmbedding f
-- Mathlib.AlgebraicGeometry.Normalization
/-- Given an qcqs morphism `f : X ⟶ Y`, which factors into `X ⟶ T ⟶ Y` with `T ⟶ Y` integral,
the map `X ⟶ T` factors through `f.normalization` uniquely.
(See `normalization.hom_ext` for the uniqueness result)  -/
AlgebraicGeometry.Scheme.Hom.normalizationDesc : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.QuasiCompact f] →
      [inst_1 : AlgebraicGeometry.QuasiSeparated f] →
        {T : AlgebraicGeometry.Scheme} →
          (f₁ : X ⟶ T) →
            (f₂ : T ⟶ Y) →
              [AlgebraicGeometry.IsIntegralHom f₂] →
                f = CategoryTheory.CategoryStruct.comp f₁ f₂ → (AlgebraicGeometry.Scheme.Hom.normalization f ⟶ T)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_map_app_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] (F : CategoryTheory.Functor C V) {G G' : CategoryTheory.Functor C V}
  (η : G ⟶ G') (c : C) (X : Cᵒᵖ) (c_1 : C),
  ((((CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor F).map η).app c).app X).app c_1 =
    (CategoryTheory.ihom (F.obj (Opposite.unop X))).map (η.app (CategoryTheory.MonoidalCategoryStruct.tensorObj c_1 c))
-- Mathlib.FieldTheory.AbelRuffini
/-- **Alias** of `isSolvable_gal_of_irreducible`.

---

**Abel-Ruffini Theorem** (one direction): An irreducible polynomial with a `solvableByRad` root
has a solvable Galois group.  -/
solvableByRad.isSolvable' : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  x ∈ solvableByRad F E → ∀ {q : Polynomial F}, Irreducible q → (Polynomial.aeval x) q = 0 → Group.IsSolvable q.Gal
-- Lean.Compiler.LCNF.Types
/-- `float32` is a 32-bit floating point number.
 -/
Lean.Compiler.LCNF.ImpureType.float32 : Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.forget_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Comon C),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Comon.forget C) X Y =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X)
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The factorisation condition.  -/
CategoryTheory.Factorisation.ι_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.Factorisation f)
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.ι (CategoryTheory.CategoryStruct.comp self.π h) =
    CategoryTheory.CategoryStruct.comp f h
-- Init.Grind.Config
/-- If `mbtc` is `true`, `grind` will use model-based theory combination for creating new case splits.
See paper "Model-based Theory Combination" for details.
 -/
Lean.Grind.Config.mbtc : Lean.Grind.Config → Bool
-- Init.Data.Array.Count
Array.count_le_count_push : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {xs : Array α}, Array.count a xs ≤ Array.count a (xs.push b)
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
Algebra.Generators.H1Cotangent.equiv.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  {ι' : Type u_1} (P : Algebra.Generators R S ι) (P' : Algebra.Generators R S ι'),
  Algebra.Generators.H1Cotangent.equiv P P' =
    Algebra.Extension.H1Cotangent.equiv (P.defaultHom P').toExtensionHom (P'.defaultHom P).toExtensionHom
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.instCanonicallyOverSpecResidueField : {X : AlgebraicGeometry.Scheme} → (x : ↥X) → (AlgebraicGeometry.Spec (X.residueField x)).CanonicallyOver X
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
TopCat.instHasIsosPrecoverage : TopCat.precoverage.HasIsos
-- Mathlib.Topology.Baire.Lemmas
/-- Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with ⋂₀.  -/
dense_sInter_of_Gδ : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] {S : Set (Set X)},
  (∀ s ∈ S, IsGδ s) → S.Countable → (∀ s ∈ S, Dense s) → Dense (⋂₀ S)
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.dvd_of_roots_le_roots : ∀ {R : Type u_1} [inst : Field R] {f g : Polynomial R}, f.Splits → f ≠ 0 → f.roots ≤ g.roots → f ∣ g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constToArray_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Internal.Impl.Const.toArray t₁ = Std.DTreeMap.Internal.Impl.Const.toArray t₂
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.match : Lean.Syntax →
  Lean.Syntax →
    Lean.Syntax → Lean.Syntax → Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.compAlongOrderedFinpartitionₗ_apply_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n)
  (f : F [×c.length]→L[𝕜] G) (p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F),
  (c.compAlongOrderedFinpartitionₗ f) p = c.compAlongOrderedFinpartition f p
-- Mathlib.Topology.Baire.BaireMeasurable
/-- Notation to say that a property of points in a topological space holds
almost everywhere in the sense of Baire category. That is, on a residual set.  -/
Topology.«term∀ᵇ_,_» : Lean.ParserDescr
-- Mathlib.Logic.Encodable.Basic
Encodable.countable : ∀ {α : Type u_1} [Encodable α], Countable α
-- Mathlib.Algebra.Group.Hom.Defs
instInhabitedMulHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : MulOneClass N], instInhabitedMulHom = { default := 1 }
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainTopIdx.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P P_1 : RootPairing ι R M N} (e_P : P = P_1) [inst_8 : P.IsCrystallographic] (i i_1 : ι),
  i = i_1 → ∀ (j j_1 : ι), j = j_1 → RootPairing.chainTopIdx i j = RootPairing.chainTopIdx i_1 j_1
-- Mathlib.Order.Atoms
IsCoatomic.Set.Ici.isCoatomic : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] [IsCoatomic α] {x : α}, IsCoatomic ↑(Set.Ici x)
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquiv_unit_app_app_inl : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (X : CategoryTheory.Functor (A ⊕ A') B) (a : A),
  ((CategoryTheory.Sum.functorEquiv A A' B).unit.app X).app (Sum.inl a) =
    CategoryTheory.CategoryStruct.id (X.obj (Sum.inl a))
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_le_iff : ∀ {R : Type u_2} [inst : NonAssocSemiring R] {S₁ : Subsemiring R} {S₂ : Subsemiring Rᵐᵒᵖ}, S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- A pointwise left Kan extension of `F` along `L` applied to an object `Y` is isomorphic to
`colimit (CostructuredArrow.proj L Y ⋙ F)`.  -/
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.isoColimit : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                {E : L.LeftExtension F} →
                  {Y : D} →
                    E.IsPointwiseLeftKanExtensionAt Y →
                      [inst_3 : CategoryTheory.Limits.HasColimit ((CategoryTheory.CostructuredArrow.proj L Y).comp F)] →
                        (CategoryTheory.StructuredArrow.right E).obj Y ≅
                          CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.proj L Y).comp F)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- Construct a bounded continuous function from a continuous function vanishing at infinity.  -/
ZeroAtInftyContinuousMap.toBCF : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace β] → [inst_2 : Zero β] → ZeroAtInftyContinuousMap α β → BoundedContinuousFunction α β
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
/-- Takes in a formula `f` and a single `ratHint` and attempts to verify that `f` is inconsistent with the
negation of the `ratHint`'s clause. It returns:
- `f` which is the same as the original `f` (including the ratUnits and assignment fields)
  - Although the `ratUnits` and `assignments` fields are updated during the procedure,
    they are restored prior to returning..
- `success`, which indicates whether empty was successfully derived without any errors

Note: This function assumes that the `ratUnits` corresponding to this rat check have NOT already
been added to `f`. In terms of input expectations and output guarantees, this function is more
analogous to `performRupAdd` than `performRupCheck`.
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatCheck : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n →
    Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      ℕ × Array ℕ → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.support_of : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (i : ι) (x : β i),
  x ≠ 0 → DFinsupp.support ((DirectSum.of β i) x) = {i}
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_sub_le : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : NormedAddCommGroup V]
  {μ ν : MeasureTheory.VectorMeasure X V}, (μ - ν).variation ≤ μ.variation + ν.variation
-- Mathlib.Tactic.NormNum.NatLog
Mathlib.Meta.NormNum.isNat_log : ∀ {b nb n nn k : ℕ},
  Mathlib.Meta.NormNum.IsNat b nb →
    Mathlib.Meta.NormNum.IsNat n nn → Nat.log nb nn = k → Mathlib.Meta.NormNum.IsNat (Nat.log b n) k
-- Lean.Util.PPExt
Lean.FormatWithInfos.mk.injEq : ∀ (fmt : Std.Format) (infos : Lean.PrettyPrinter.InfoPerPos) (fmt_1 : Std.Format)
  (infos_1 : Lean.PrettyPrinter.InfoPerPos),
  ({ fmt := fmt, infos := infos } = { fmt := fmt_1, infos := infos_1 }) = (fmt = fmt_1 ∧ infos = infos_1)
-- Init.Data.UInt.Bitwise
UInt8.shiftRight_xor : ∀ {a b c : UInt8}, (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
-- Mathlib.Topology.Category.TopCat.OpenNhds
/-- An open embedding `f : X ⟶ Y` induces a functor `OpenNhds x ⥤ OpenNhds (f x)`.
We define `IsOpenEmbedding.functorNhds` as `IsOpenEmbedding.isOpenMap.functorNds`, so it won't
default to `IsInducing.functorNhds` (which is equal but not defeq).
 -/
Topology.IsOpenEmbedding.functorNhds : {X Y : TopCat} →
  {f : X ⟶ Y} →
    Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) →
      (x : ↑X) →
        CategoryTheory.Functor (TopologicalSpace.OpenNhds x)
          (TopologicalSpace.OpenNhds ((CategoryTheory.ConcreteCategory.hom f) x))
-- Mathlib.CategoryTheory.GradedObject
/-- A type synonym for `β → C`, used for `β`-graded objects in a category `C`
with a shift functor given by translation by `s`.
 -/
CategoryTheory.GradedObjectWithShift : {β : Type w} → [AddCommGroup β] → β → Type u → Type (max w u)
-- Mathlib.Data.List.Basic
List.mem_dropLast_of_mem_of_ne_getLastD : ∀ {α : Type u} {l : List α} {a d : α}, a ∈ l → a ≠ l.getLastD d → a ∈ l.dropLast
-- Init.Data.BitVec.Bootstrap
BitVec.cons_msb_setWidth : ∀ {w : ℕ} (x : BitVec (w + 1)), BitVec.cons x.msb (BitVec.setWidth w x) = x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
opposite side, version subtracting vectors.  -/
Orientation.sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle y (y - x)).sin * ‖y - x‖ = ‖x‖
-- Mathlib.Topology.VectorBundle.Constructions
Bundle.Trivial.continuousLinearEquivAt_trivialization : ∀ (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace B] (x : B),
  Bundle.Trivialization.continuousLinearEquivAt 𝕜 (Bundle.Trivial.trivialization B F) x ⋯ =
    ContinuousLinearEquiv.refl 𝕜 F
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_vecMulVec : ∀ {n : Type u_3} {R : Type u_6} [inst : Fintype n] [inst_1 : NonUnitalNonAssocSemiring R] (a b : n → R),
  (Matrix.vecMulVec a b).trace = a ⬝ᵥ b
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.IsSeparator.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsSeparator G = (CategoryTheory.ObjectProperty.singleton G).IsSeparating
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom_assoc : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c₁ c₂ c₃ : C) (d : D) {Z : D}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c₁
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c₂
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c₃ d)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
        (CategoryTheory.MonoidalCategoryStruct.associator c₁ c₂ c₃).hom d)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₁
            (CategoryTheory.MonoidalCategoryStruct.tensorObj c₂ c₃) d).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c₁
            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₂ c₃ d).hom)
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso
          (CategoryTheory.MonoidalCategoryStruct.tensorObj c₁ c₂) c₃ d).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₁ c₂
            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c₃ d)).hom
        h)
-- Mathlib.Tactic.IntervalCases
/-- A less-than-or-equal lower bound `n ≤ e` or upper bound `e ≤ n`.  -/
Mathlib.Tactic.IntervalCases.Bound.le : ℤ → Mathlib.Tactic.IntervalCases.Bound
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.instIsFaithfulOfHasTrivialRadical : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.HasTrivialRadical R L], LieModule.IsFaithful R L L
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.findKeyDAtAux : {α : Type u_1} → {β : Type u_2} → [BEq α] → (keys : Array α) → (vals : Array β) → keys.size = vals.size → ℕ → α → α → α
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.instInhabitedPattern.default : Lean.Meta.Sym.Pattern
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExtractCoeff.mk.injEq : ∀ {e : Q(ℕ)} (k e' : Q(ℕ)) (ve' : Mathlib.Tactic.Ring.Common.ExProdNat e') (p : Q(«$e» = «$e'» * «$k»))
  (k_1 e'_1 : Q(ℕ)) (ve'_1 : Mathlib.Tactic.Ring.Common.ExProdNat e'_1) (p_1 : Q(«$e» = «$e'_1» * «$k_1»)),
  ({ k := k, e' := e', ve' := ve', p := p } = { k := k_1, e' := e'_1, ve' := ve'_1, p := p_1 }) =
    (k = k_1 ∧ e' = e'_1 ∧ ve' ≍ ve'_1 ∧ p = p_1)
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.sub_apply : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Ring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : IsTopologicalAddGroup F]
  [inst_10 : ContinuousConstSMul 𝕜 F] (f g : FormalMultilinearSeries 𝕜 E F) (n : ℕ), (f - g) n = f n - g n
-- Mathlib.CategoryTheory.Localization.Construction
/-- The unit isomorphism of the equivalence of categories `whiskeringLeftEquivalence W D`.  -/
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (D : Type uD) →
        [inst_1 : CategoryTheory.Category.{uD', uD} D] →
          CategoryTheory.Functor.id (CategoryTheory.Functor W.Localization D) ≅
            (CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D).comp
              (CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D)
-- Init.Data.Int.Order
Int.ofNat_nonneg : ∀ (n : ℕ), 0 ≤ ↑n