mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.VectorBundle.Constructions
Bundle.Trivialization.coordChangeL_prod : ∀ (𝕜 : Type u_1) {B : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : TopologicalSpace B] {F₁ : Type u_3}
  [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] {E₁ : B → Type u_4}
  [inst_4 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_5} [inst_5 : NormedAddCommGroup F₂]
  [inst_6 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_6} [inst_7 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_8 : (x : B) → AddCommMonoid (E₁ x)] [inst_9 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_10 : (x : B) → AddCommMonoid (E₂ x)] [inst_11 : (x : B) → Module 𝕜 (E₂ x)]
  (e₁ e₁' : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e₂ e₂' : Bundle.Trivialization F₂ Bundle.TotalSpace.proj)
  [inst_12 : Bundle.Trivialization.IsLinear 𝕜 e₁] [inst_13 : Bundle.Trivialization.IsLinear 𝕜 e₁']
  [inst_14 : Bundle.Trivialization.IsLinear 𝕜 e₂] [inst_15 : Bundle.Trivialization.IsLinear 𝕜 e₂'] ⦃b : B⦄,
  (b ∈ e₁.baseSet ∧ b ∈ e₂.baseSet) ∧ b ∈ e₁'.baseSet ∧ b ∈ e₂'.baseSet →
    ↑(Bundle.Trivialization.coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) =
      (↑(Bundle.Trivialization.coordChangeL 𝕜 e₁ e₁' b)).prodMap ↑(Bundle.Trivialization.coordChangeL 𝕜 e₂ e₂' b)
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
/-- The derivative `D_yf(y)` is `C^m` at `x₀`, where the derivative is taken as a continuous
linear map. We have to assume that `f` is `C^n` at `x₀` for some `n ≥ m + 1`.
We have to insert a coordinate change from `x₀` to `x` to make the derivative sensible.
This is a special case of `ContMDiffWithinAt.mfderivWithin` where `f` does not contain any
parameters and `g = id`.
 -/
ContMDiffWithinAt.mfderivWithin_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {m n : WithTop ℕ∞} {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'] {s : Set M} [Is : IsManifold I 1 M]
  [I's : IsManifold I' 1 M'] {x₀ : M} {f : M → M'},
  ContMDiffWithinAt I I' n f s x₀ →
    m + 1 ≤ n →
      x₀ ∈ s →
        UniqueMDiff[s] →
          ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (E →L[𝕜] E')) m (inTangentCoordinates I I' id f (mfderiv[s] f) x₀)
            s x₀
-- Mathlib.Computability.RegularExpressions
RegularExpression.matchEpsilon.eq_2 : ∀ {α : Type u_1}, RegularExpression.epsilon.matchEpsilon = true
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyGT_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} {h' : ∃ a ∈ t₁, cmp a k = Ordering.gt} (h : t₁.Equiv t₂), t₁.getKeyGT k h' = t₂.getKeyGT k ⋯
-- Mathlib.Algebra.Polynomial.FieldDivision
/-- If `f` is a polynomial over a field, and `a : K` satisfies `f' a ≠ 0`,
then `f / (X - a)` is coprime with `X - a`.
Note that we do not assume `f a = 0`, because `f / (X - a) = (f - f a) / (X - a)`.  -/
Polynomial.isCoprime_of_is_root_of_eval_derivative_ne_zero : ∀ {K : Type u_1} [inst : Field K] (f : Polynomial K) (a : K),
  Polynomial.eval a (Polynomial.derivative f) ≠ 0 →
    IsCoprime (Polynomial.X - Polynomial.C a) (f /ₘ (Polynomial.X - Polynomial.C a))
-- Mathlib.NumberTheory.Divisors
Nat.castEmbedding.congr_simp : ∀ {R : Type u_2} [inst : AddMonoidWithOne R] [inst_1 : CharZero R], Nat.castEmbedding = Nat.castEmbedding
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.snd_comp_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
  Monoid.Coprod.snd.comp Monoid.Coprod.inr = MonoidHom.id N
-- Init.Data.Option.Lemmas
/-- The `simp` normal form of `o <|> o'` is `o.or o'` via `orElse_eq_orElse` and `orElse_eq_or`.  -/
Option.orElse_eq_orElse : ∀ {α : Type u_1}, HOrElse.hOrElse = Option.orElse
-- Mathlib.Order.JordanHolder
CompositionSeries.lt_last_of_mem_eraseLast : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s : CompositionSeries X} {x : X},
  0 < s.length → x ∈ RelSeries.eraseLast s → x < RelSeries.last s
-- Init.Data.Rat.Lemmas
Rat.num_inv : ∀ (a : ℚ), a⁻¹.num = a.num.sign * ↑a.den
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.val_of : ∀ {M : Type u_1} (a : M), MulArchimedeanOrder.val (MulArchimedeanOrder.of a) = a
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.mk.injEq : ∀ (carrier : Type u) [str : Monoid carrier] (carrier_1 : Type u) (str_1 : Monoid carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.request : Lean.JsonRpc.RequestID → String → Lean.JsonRpc.MessageMetaData
-- Mathlib.Algebra.Category.Grp.Limits
/-- A functor `F : J ⥤ AddCommGrpCat.{u}` has a limit iff
`(F ⋙ forget AddCommGrpCat).sections` is `u`-small.  -/
AddCommGrpCat.hasLimit_iff_small_sections : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat),
  CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.lift_add : ∀ {α : Type u} {G : Type u_1} [inst : AddCommGroup G] (f g : α → G),
  FreeAbelianGroup.lift (f + g) = FreeAbelianGroup.lift f + FreeAbelianGroup.lift g
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.RightExactFunctor.of_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.PreservesFiniteColimits F],
  (CategoryTheory.RightExactFunctor.of F).obj = F
-- Mathlib.RingTheory.Norm.Basic
IntermediateField.AdjoinSimple.norm_gen_eq_one : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L},
  ¬IsIntegral K x → (Algebra.norm K) (IntermediateField.AdjoinSimple.gen K x) = 1
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.codChart.congr_simp : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G]
  {I I_1 : ModelWithCorners 𝕜 E H} (e_I : I = I_1) {J J_1 : ModelWithCorners 𝕜 E'' G} (e_J : J = J_1) {M : Type u_11}
  {N : Type u_13} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N]
  [inst_12 : ChartedSpace G N] {n n_1 : WithTop ℕ∞} (e_n : n = n_1) {f f_1 : M → N} (e_f : f = f_1) {x x_1 : M}
  (e_x : x = x_1) (h : Manifold.IsSubmersionAtOfComplement F I J n f x), h.codChart = ⋯.codChart
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.interSmaller.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (m₁ m₂ : Std.DTreeMap.Internal.Impl α β),
  m₁.interSmaller m₂ =
    ↑(Std.DTreeMap.Internal.Impl.foldl (fun sofar k x => m₁.interSmallerFn sofar k)
        ⟨Std.DTreeMap.Internal.Impl.empty, ⋯⟩ m₂)
-- Mathlib.CategoryTheory.Action.Basic
Action.Iso.conj_ρ : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (f : M ≅ N) (g : G), N.ρ g = ((Action.forget V G).mapIso f).conj (M.ρ g)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_monomial : ∀ {R : Type u} {a : R} [inst : Semiring R] (n : ℕ), a ≠ 0 → ((Polynomial.monomial n) a).degree = ↑n
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDeriv_singularPart : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ ν : ProbabilityTheory.Kernel α γ)
  [inst : ProbabilityTheory.IsFiniteKernel κ] [inst_1 : ProbabilityTheory.IsFiniteKernel ν] (a : α),
  (κ.singularPart ν).rnDeriv ν a =ᵐ[ν a] 0
-- Init.Data.UInt.Lemmas
UInt64.toNat_toBitVec : ∀ (x : UInt64), x.toBitVec.toNat = x.toNat
-- Mathlib.Data.Finset.Image
Finset.image_inj : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s t : Finset α},
  Function.Injective f → (Finset.image f s = Finset.image f t ↔ s = t)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α} {h : k ∈ Std.DHashMap.filterMap f m},
  Std.DHashMap.Const.get (Std.DHashMap.filterMap f m) k h = (f (m.getKey k ⋯) (Std.DHashMap.Const.get m k ⋯)).get ⋯
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_surjective : ∀ {n : ℕ}, Function.Surjective Int.cast
-- Mathlib.Algebra.Group.Center
IsAddCentral.mid_assoc : ∀ {M : Type u_1} [inst : Add M] {z : M}, IsAddCentral z → ∀ (a c : M), a + z + c = a + (z + c)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.eta_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (t : CategoryTheory.Limits.PushoutCocone f g), t.eta.hom.hom = CategoryTheory.CategoryStruct.id t.pt
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.instEpiCommRingCatResidue : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (x : ↑X.toTopCat), CategoryTheory.Epi (X.residue x)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLE.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x_3 : Std.DTreeMap.Internal.Impl.leaf.Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isLE = true),
  Std.DTreeMap.Internal.Impl.Const.getEntryLE k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
/-- The rank of a module `M` at a prime `p` is equal to the dimension
of `κ(p) ⊗[R] M` as a `κ(p)`-module.  -/
Module.rankAtStalk_eq : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  [Module.Finite R M] (p : PrimeSpectrum R),
  Module.rankAtStalk M p = Module.finrank p.asIdeal.ResidueField (p.asIdeal.Fiber M)
-- Std.Async.System
/-- The user's login shell.
 -/
Std.Async.System.SystemUser.shell : Std.Async.System.SystemUser → Option String
-- Batteries.Lean.AttributeExtra
/-- A list of "base" declarations which have been pre-tagged.  -/
Lean.TagAttributeExtra.base : Lean.TagAttributeExtra → Lean.NameHashSet
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_mul_single_mul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Monoid M] [IsCancelMul M] (x : MonoidAlgebra R M) (r : R)
  (m m' : M), (x * MonoidAlgebra.single m r).coeff (m' * m) = x.coeff m' * r
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.empty_toList : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)], Monoid.CoprodI.Word.empty.toList = []
-- Mathlib.Computability.TuringMachine.Computable
/-- a proof this machine outputs `f`  -/
Turing.TM2Computable.outputsFun : {α β αΓ βΓ : Type} →
  {ea : α → List αΓ} →
    {eb : β → List βΓ} →
      {f : α → β} →
        (self : Turing.TM2Computable ea eb f) →
          (a : α) →
            Turing.TM2Outputs self.tm (List.map self.inputAlphabet.invFun (ea a))
              (some (List.map self.outputAlphabet.invFun (eb (f a))))
-- Mathlib.GroupTheory.CosetCover
/-- Let the group `G` be the union of finitely many left cosets `g i • H i`.
Then the cosets of subgroups of infinite index may be omitted from the covering.  -/
Subgroup.leftCoset_cover_filter_FiniteIndex : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
    ∀ [inst_1 : DecidablePred Subgroup.FiniteIndex], ⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • ↑(H k) = Set.univ
-- Mathlib.SetTheory.ZFC.Rank
PSet.rank_singleton : ∀ (x : PSet.{u_1}), {x}.rank = Order.succ x.rank
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.ofSet_trans : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : IsOpen s), (OpenPartialHomeomorph.ofSet s hs).trans e = e.restr s
-- Mathlib.Order.UpperLower.Principal
LowerSet.mem_Iic_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ∈ LowerSet.Iic a ↔ b ≤ a
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- Mapping a presentation under an isomorphism.  -/
SheafOfModules.Presentation.ofIsIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {M N : SheafOfModules R} → (f : M ⟶ N) → [CategoryTheory.IsIso f] → M.Presentation → N.Presentation
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.range_toContinuousMap : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B],
  Set.range ContinuousMonoidHom.toContinuousMap = {f | f 1 = 1 ∧ ∀ (x y : A), f (x * y) = f x * f y}
-- Init.Data.UInt.BasicAux
/-- Subtracts one 32-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the `-` operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.sub : UInt32 → UInt32 → UInt32
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.refl_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X], (Homeomorph.refl X).symm = Homeomorph.refl X
-- Mathlib.Data.FinEnum.Option
/-- Inserting an `Option.none` anywhere in an enumeration yields another enumeration.  -/
FinEnum.insertNone : (α : Type u) → [inst : FinEnum α] → Fin (FinEnum.card α + 1) → FinEnum (Option α)
-- Std.Http.Data.Headers.Value
Std.Http.Header.Value.mk.inj : ∀ {value : String}
  {isValidHeaderValue :
    autoParam (Std.Http.Header.IsValidHeaderValue value) Std.Http.Header.Value.isValidHeaderValue._autoParam}
  {value_1 : String}
  {isValidHeaderValue_1 :
    autoParam (Std.Http.Header.IsValidHeaderValue value_1) Std.Http.Header.Value.isValidHeaderValue._autoParam},
  { value := value, isValidHeaderValue := isValidHeaderValue } =
      { value := value_1, isValidHeaderValue := isValidHeaderValue_1 } →
    value = value_1
-- Std.Sat.AIG.Basic
/-- Add a new and inverter gate to the AIG in `aig`. Note that this version is only meant for proving,
for production purposes use `AIG.mkGateCached` and equality theorems to this one.
 -/
Std.Sat.AIG.mkGate : {α : Type} →
  [inst : Hashable α] → [inst_1 : DecidableEq α] → (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommProd_cons : ∀ {α : Type u_3} [inst : Monoid α] (s : Multiset α) (a : α) (comm : {x | x ∈ a ::ₘ s}.Pairwise Commute),
  (a ::ₘ s).noncommProd comm = a * s.noncommProd ⋯
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- In a Polish space, a set is clopenable if and only if it is Borel-measurable.  -/
MeasureTheory.isClopenable_iff_measurableSet : ∀ {γ : Type u_3} {s : Set γ} [tγ : TopologicalSpace γ] [PolishSpace γ] [inst : MeasurableSpace γ] [BorelSpace γ],
  PolishSpace.IsClopenable s ↔ MeasurableSet s
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalysisNeedsType : Lean.Options → Bool
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Functor.toProfunctor_obj_map : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C) {X_1 Y : Dᵒᵖ} (f : X_1 ⟶ Y),
  (F.toProfunctor.obj X).map f = TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp f.unop g
-- Mathlib.Topology.VectorBundle.Basic
/-- The zero section of a vector bundle  -/
Bundle.zeroSection : {B : Type u_2} → (F : Type u_3) → (E : B → Type u_4) → [(x : B) → Zero (E x)] → B → Bundle.TotalSpace F E
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.HasInjectiveResolution.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C},
  Nonempty (CategoryTheory.InjectiveResolution Z) → CategoryTheory.HasInjectiveResolution Z
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.GrpObjAsOverPullback : {M S T : AlgebraicGeometry.Scheme} →
  [inst : M.Over S] →
    {f : T ⟶ S} →
      [CategoryTheory.GrpObj (M.asOver S)] → CategoryTheory.GrpObj ((CategoryTheory.Limits.pullback (M ↘ S) f).asOver T)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castAddEmb_Ici : ∀ {n : ℕ} (m : ℕ) [inst : NeZero m] (i : Fin n),
  Finset.map (Fin.castAddEmb m) (Finset.Ici i) = Finset.Ico (Fin.castAdd m i) (Fin.natAdd n 0)
-- Mathlib.Algebra.Polynomial.PartialFractions
/-- **Alias** of `Polynomial.div_eq_quo_add_rem_div_add_rem_div`.

---

Let `R` be an integral domain and `f, g₁, g₂ : R[X]`. Let `g₁` and `g₂` be monic and coprime.
Then `∃ q, r₁, r₂ : R[X]` such that `f / (g₁ * g₂) = q + r₁ / g₁ + r₂ / g₂` and
`degree rᵢ < degree gᵢ`, where the equality is taken in a field `K` containing `R[X]`.
See `quo_add_rem_div_add_rem_div_unique` for the uniqueness of this representation.  -/
div_eq_quo_add_rem_div_add_rem_div : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra (Polynomial R) K]
  [FaithfulSMul (Polynomial R) K] (f : Polynomial R) {g₁ g₂ : Polynomial R},
  g₁.Monic →
    g₂.Monic →
      IsCoprime g₁ g₂ →
        ∃ q r₁ r₂, r₁.degree < g₁.degree ∧ r₂.degree < g₂.degree ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.iSup_induction : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {ι : Sort u_1}
  (S : ι → Subalgebra R A) {motive : A → Prop} {x : A},
  x ∈ ⨆ i, S i →
    (∀ (i : ι), ∀ a ∈ S i, motive a) →
      (∀ (a b : A), motive a → motive b → motive (a + b)) →
        (∀ (a b : A), motive a → motive b → motive (a * b)) → (∀ (r : R), motive ((algebraMap R A) r)) → motive x
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.aeval : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  {φ : MvPolynomial σ R} {m n : ℕ} [inst_2 : Algebra R S],
  φ.IsHomogeneous m →
    ∀ (g : σ → MvPolynomial τ S), (∀ (i : σ), (g i).IsHomogeneous n) → ((MvPolynomial.aeval g) φ).IsHomogeneous (n * m)
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.errorName : Lean.Syntax → Lean.Syntax → Lean.Elab.CompletionInfo
-- Mathlib.Condensed.Light.TopCatAdjunction
LightCondSet.continuous_coinducingCoprod : ∀ (X : LightCondSet) {S : LightProfinite} (x : X.obj.obj (Opposite.op S)),
  Continuous fun a => LightCondSet.coinducingCoprod✝ X ⟨⟨S, x⟩, a⟩
-- Batteries.Data.List.Lemmas
List.replaceF_nil : ∀ {α : Type u_1} {p : α → Option α}, List.replaceF p [] = []
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.instCommMonoidWithZero : {R : Type u_2} →
  [inst : CommSemiring R] → [inst_1 : PartialOrder R] → [IsOrderedRing R] → CommMonoidWithZero ↑(Set.Icc 0 1)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_prod : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β},
  MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
-- Mathlib.Algebra.Quaternion
Quaternion.mul_star_eq_coe : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), a * star a = ↑(a * star a).re
-- Mathlib.Order.Max
Prod.isMin_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsMin x ↔ IsMin x.1 ∧ IsMin x.2
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.sliceFrom_lt_sliceFrom_iff : ∀ {s : String.Slice} {p₀ q r : s.Pos} {h₁ : p₀ ≤ q} {h₂ : p₀ ≤ r}, p₀.sliceFrom q h₁ < p₀.sliceFrom r h₂ ↔ q < r
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₃₂_single_one_snd : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g h : G) (a : ↑A),
  ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₃₂ A)) fun₀ | (g, 1, h) => a) =
    (fun₀ | (1, h) => (A.ρ g⁻¹) a) - fun₀ | (g, 1) => a
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of a constant function is `⊤` if the constant is zero and `0` otherwise.
 -/
meromorphicOrderAt_const_ofNat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] (z₀ : 𝕜) (n : ℕ) [inst_3 : Decidable (↑n = 0)],
  meromorphicOrderAt (OfNat.ofNat n) z₀ = if ↑n = 0 then ⊤ else 0
-- Mathlib.Topology.Semicontinuity.Basic
ContinuousAt.comp_upperSemicontinuousAt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
  [OrderTopology δ] {g : γ → δ} {f : α → γ},
  ContinuousAt g (f x) → UpperSemicontinuousAt f x → Monotone g → UpperSemicontinuousAt (g ∘ f) x
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.mk.inj : ∀ {arr : Array Batteries.UFNode} {parentD_lt : ∀ {i : ℕ}, i < arr.size → Batteries.UnionFind.parentD arr i < arr.size}
  {rankD_lt :
    ∀ {i : ℕ},
      Batteries.UnionFind.parentD arr i ≠ i →
        Batteries.UnionFind.rankD arr i < Batteries.UnionFind.rankD arr (Batteries.UnionFind.parentD arr i)}
  {arr_1 : Array Batteries.UFNode}
  {parentD_lt_1 : ∀ {i : ℕ}, i < arr_1.size → Batteries.UnionFind.parentD arr_1 i < arr_1.size}
  {rankD_lt_1 :
    ∀ {i : ℕ},
      Batteries.UnionFind.parentD arr_1 i ≠ i →
        Batteries.UnionFind.rankD arr_1 i < Batteries.UnionFind.rankD arr_1 (Batteries.UnionFind.parentD arr_1 i)},
  { arr := arr, parentD_lt := parentD_lt, rankD_lt := rankD_lt } =
      { arr := arr_1, parentD_lt := parentD_lt_1, rankD_lt := rankD_lt_1 } →
    arr = arr_1
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.ppActiveTheoremPatterns : Lean.Meta.Grind.M✝ Unit
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The sigma type of all `E.I₁ i₁ i₂` for `⟨i₁, i₂⟩ : E.I₀ × E.I₀`.  -/
CategoryTheory.PreOneHypercover.I₁' : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {S : C} → CategoryTheory.PreOneHypercover S → Type w
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The category of additive monoids and monoid morphisms.  -/
AddMonCat : Type (u + 1)
-- Mathlib.Data.List.Basic
List.filter_singleton : ∀ {α : Type u} {p : α → Bool} {a : α}, List.filter p [a] = bif p a then [a] else []
-- Lean.Parser.Basic
Lean.Parser.errorFn : String → Lean.Parser.ParserFn
-- Mathlib.Data.List.NodupEquivFin
/-- A `l : List α` is `Sublist l l'` for `l' : List α` iff
there is `f`, an order-preserving embedding of `Fin l.length` into `Fin l'.length` such that
any element of `l` found at index `ix` can be found at index `f ix` in `l'`.
 -/
List.sublist_iff_exists_fin_orderEmbedding_get_eq : ∀ {α : Type u_1} {l l' : List α}, l.Sublist l' ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.mk.injEq : ∀ {α : Type u_8} {β : Type u_9} [inst : InfSet α] [inst_1 : InfSet β] (toFun : α → β)
  (map_sInf' : ∀ (s : Set α), toFun (sInf s) = sInf (toFun '' s)) (toFun_1 : α → β)
  (map_sInf'_1 : ∀ (s : Set α), toFun_1 (sInf s) = sInf (toFun_1 '' s)),
  ({ toFun := toFun, map_sInf' := map_sInf' } = { toFun := toFun_1, map_sInf' := map_sInf'_1 }) = (toFun = toFun_1)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Multipliable.map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [inst_2 : CommMonoid γ] [inst_3 : TopologicalSpace γ],
  Multipliable f L →
    ∀ {G : Type u_4} [inst_4 : FunLike G α γ] [MonoidHomClass G α γ] (g : G), Continuous ⇑g → Multipliable (⇑g ∘ f) L