mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- Localization commutes with ranges.  -/
LinearMap.localized'_range_eq_range_localizedMap : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f] {P : Type u_5}
  [inst_11 : AddCommMonoid P] [inst_12 : Module R P] {Q : Type u_6} [inst_13 : AddCommMonoid Q] [inst_14 : Module R Q]
  [inst_15 : Module S Q] [inst_16 : IsScalarTower R S Q] (f' : P →ₗ[R] Q) [inst_17 : IsLocalizedModule p f']
  (g : M →ₗ[R] P),
  Submodule.localized' S p f' g.range =
    (LinearMap.extendScalarsOfIsLocalization p S ((IsLocalizedModule.map p f f') g)).range
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pushforward_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Sieve Y) (x : C)
  (gf : x ⟶ X),
  (CategoryTheory.Sieve.pushforward f R).arrows gf = ∃ g, CategoryTheory.CategoryStruct.comp g f = gf ∧ R.arrows g
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
/-- Up to equivalence, `LieAlgebra.IsKilling.rootSystem` is left inverse to
`RootPairing.GeckConstruction.lieAlgebra`.  -/
RootPairing.GeckConstruction.equivRootSystem : {ι : Type u_1} →
  {K : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : Fintype ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : Field K] →
              [inst_3 : CharZero K] →
                [inst_4 : AddCommGroup M] →
                  [inst_5 : Module K M] →
                    [inst_6 : AddCommGroup N] →
                      [inst_7 : Module K N] →
                        {P : RootPairing ι K M N} →
                          [inst_8 : P.IsReduced] →
                            [inst_9 : P.IsCrystallographic] →
                              [inst_10 : P.IsIrreducible] →
                                [inst_11 : P.IsRootSystem] →
                                  (b : P.Base) →
                                    [inst_12 : IsAlgClosed K] →
                                      P.Equiv
                                        (LieAlgebra.IsKilling.rootSystem
                                          (RootPairing.GeckConstruction.cartanSubalgebra' b))
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{t, w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  {X : C} {K : Type s} [inst_3 : CategoryTheory.SmallCategory K]
  {F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)} {W : J.Cover X} (i : W.Arrow)
  (E :
    CategoryTheory.Limits.Cone
      (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj (Opposite.op W))))),
  (CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation i E).pt = E.pt
-- Init.GrindInstances.ToInt
Lean.Grind.instModUInt8UintOfNatNat : Lean.Grind.ToInt.Mod UInt8 (Lean.Grind.IntInterval.uint 8)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- The diagram of finite quotients of `P` viewed in `ProfiniteGrp`.  -/
ProfiniteGrp.diagram : (P : ProfiniteGrp.{u}) → CategoryTheory.Functor (OpenNormalSubgroup ↑P.toProfinite.toTop) ProfiniteGrp.{u}
-- Mathlib.Data.Finsupp.Basic
Finsupp.comapDomain.addMonoidHom_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddZeroClass M] {f : α → β} (hf : Function.Injective f)
  (x : β →₀ M), (Finsupp.comapDomain.addMonoidHom hf) x = Finsupp.comapDomain f x ⋯
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.vId_iso_hom_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] (T : CategoryTheory.Functor C₁ C₂) (X : C₁),
  (CategoryTheory.CatCommSq.iso T (CategoryTheory.Functor.id C₁) (CategoryTheory.Functor.id C₂) T).hom.app X =
    CategoryTheory.CategoryStruct.id (T.obj X)
-- Mathlib.GroupTheory.Sylow
Sylow.biSup_of_normal : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {ι : Type u_2} (s : Set ι) (H : ι → Subgroup G),
  (∀ i ∈ s, IsPGroup p ↥(H i)) → (∀ i ∈ s, (H i).Normal) → IsPGroup p ↥(⨆ i ∈ s, H i)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity`.

---

The map `normalizedFactorsEquivOfQuotEquiv` preserves multiplicities.  -/
normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} [inst_3 : IsDedekindDomain R] (f : R ⧸ I ≃+* A ⧸ J) (hI : I ≠ ⊥) (hJ : J ≠ ⊥) (L : Ideal R)
  (hL : L ∈ UniqueFactorizationMonoid.normalizedFactors I),
  emultiplicity (↑((IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv f hI hJ) ⟨L, hL⟩)) J = emultiplicity L I
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.hp₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (self : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp self.chosenPullback.p₁ h₁₂.p₁ = self.p₁
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.Extension.frob.eq_1 : ∀ (k : Type u_1) [inst : Field k] [inst_1 : Finite k] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP k p] (n : ℕ)
  [inst_4 : NeZero n],
  FiniteField.Extension.frob k p n = FiniteField.frobeniusAlgEquivOfAlgebraic k (FiniteField.Extension k p n)
-- Mathlib.Topology.UniformSpace.Defs
tendsto_const_uniformity : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {a : α} {f : Filter β},
  Filter.Tendsto (fun x => (a, a)) f (uniformity α)
-- Mathlib.Data.List.MinMax
List.argmax_concat : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableLT β] (f : α → β) (a : α) (l : List α),
  List.argmax f (l ++ [a]) = Option.casesOn (List.argmax f l) (some a) fun c => if f c < f a then some a else some c
-- Batteries.Data.List.Lemmas
List.findIdxs_start : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {s : ℕ},
  List.findIdxs p xs s = List.map (fun x => x + s) (List.findIdxs p xs)
-- Init.Data.String.Basic
String.Slice.Pos.str_le_endExclusive : ∀ {s : String.Slice} (p : s.Pos), p.str ≤ s.endExclusive
-- Mathlib.Order.Hom.Basic
ULift.orderIso_apply : ∀ {α : Type u} [inst : Preorder α] (self : ULift.{v, u} α), ULift.orderIso.{v, u} self = self.down
-- Mathlib.Tactic.DefEqTransformations
/-- `eta_struct at loc` transforms structure constructor applications such as `S.mk x.1 ... x.n`
(pretty printed as, for example, `{a := x.a, b := x.b, ...}`) into `x`.
This also exists as a `conv`-mode tactic.

The transformation is known as eta reduction for structures, and it yields definitionally
equal expressions.

For example, given `x : α × β`, then `(x.1, x.2)` becomes `x` after this transformation.
 -/
Mathlib.Tactic.etaStructStx : Lean.ParserDescr
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- Given a functor from `C` to `D`, this is the corresponding profunctor from `D` to `C`.  -/
CategoryTheory.Functor.toProfunctorRev : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.Profunctor.{v₂, v₂, v₁, u₂, u₁} D C
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_const_const : ∀ {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [inst : Norm E] [inst_1 : NormedAddCommGroup F''] (c : E) {c' : F''},
  c' ≠ 0 → ∀ (l : Filter α), Asymptotics.IsBigOWith (‖c‖ / ‖c'‖) l (fun _x => c) fun _x => c'
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.ForgetCreatesColimits.γ_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (j : J),
  CategoryTheory.Monad.ForgetCreatesColimits.γ.app j = (D.obj j).a
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.characteristic_iSup : ∀ {G : Type u_1} [inst : Group G] {ι : Sort u_5} {H : ι → Subgroup G} [∀ (i : ι), (H i).Characteristic],
  (⨆ i, H i).Characteristic
-- Init.Data.Vector.Monadic
/-- We can express a for loop over a vector which always yields as a fold.  -/
Vector.forIn_yield_eq_foldlM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β γ : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  (f : α → β → m γ) (g : α → β → γ → β) (init : β),
  (forIn xs init fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) =
    Vector.foldlM (fun b a => g a b <$> f a b) init xs
-- Lean.Server.InfoUtils
/-- Elaborator information with elaborator context.

It can be thought of as a "thunked" elaboration computation that allows us
to retroactively extract type information, symbol locations, etc.
through arbitrary invocations of `runMetaM` (where the necessary context and state
can be reconstructed from `ctx` and `info.lctx`).

W.r.t. widgets, this is used to tag different parts of expressions in `ppExprTagged`.
This is the input to the RPC call `Lean.Widget.InteractiveDiagnostics.infoToInteractive`.
It carries over information about delaborated
`Info` nodes in a `CodeWithInfos`, and the associated pretty-printing
functionality is purpose-specific to showing the contents of infoview popups.

For use in standard LSP go-to-definition (see `Lean.Server.FileWorker.locationLinksOfInfo`),
all the elaborator information we need for similar tasks is already fully recoverable via
the `InfoTree` structure (see `Lean.Elab.InfoTree.visitM`).
There we use this as a convenience wrapper for queried nodes (e.g. the return value of
`Lean.Elab.InfoTree.hoverableInfoAt?`). It also includes the children info nodes
as additional context (this is unused in the RPC case, as delaboration has no notion of child nodes).

NOTE: This type is for internal use in the infoview/LSP. It should not be used in user widgets.
 -/
Lean.Elab.InfoWithCtx : Type
-- Mathlib.LinearAlgebra.Matrix.Reindex
/-- **Alias** of `Matrix.reindexLinearEquiv_trans_reindexLinearEquiv`. -/
Matrix.reindexLinearEquiv_trans : ∀ {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} {m'' : Type u_9} {n'' : Type u_10} (R : Type u_11)
  (A : Type u_12) [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] (e₁ : m ≃ m') (e₂ : n ≃ n')
  (e₁' : m' ≃ m'') (e₂' : n' ≃ n''),
  Matrix.reindexLinearEquiv R A e₁ e₂ ≪≫ₗ Matrix.reindexLinearEquiv R A e₁' e₂' =
    Matrix.reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- A `RecCallWithContext` focuses on a single recursive call in a unary predefinition,
and runs the given action in the context of that call.   -/
Lean.Elab.WF.GuessLex.RecCallWithContext : Type
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- **Alias** of the forward direction of `LinearMap.hasNoetherianRange_iff_range`. -/
LinearMap.HasNoetherianRange.isNoetherian_range : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] {f : V →ₗ[K] V₂}, f.HasNoetherianRange → IsNoetherian K ↥f.range
-- Mathlib.Data.Set.Function
Set.SurjOn.union : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} {f : α → β},
  Set.SurjOn f s t₁ → Set.SurjOn f s t₂ → Set.SurjOn f s (t₁ ∪ t₂)
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.coe_addLeft : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : SeparatelyContinuousAdd G] (a : G),
  ⇑(Homeomorph.addLeft a) = fun x => a + x
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.comonEquivalence_inverse : ∀ (R : Type u) [inst : CommRing R], (CoalgCat.comonEquivalence R).inverse = CoalgCat.ofComon R
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.ker_toLin'_eq_bot_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  {M : Matrix n n R}, (Matrix.toLin' M).ker = ⊥ ↔ ∀ (v : n → R), M.mulVec v = 0 → v = 0
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftMonoidWithZeroHom_apply_div : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} [inst_2 : CommGroupWithZero L]
  (φ : Polynomial K →*₀ L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L))
  (p q : Polynomial K),
  (RatFunc.liftMonoidWithZeroHom φ hφ)
      ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) =
    φ p / φ q
-- Mathlib.Algebra.Squarefree.Basic
IsRadical.squarefree : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsCancelMulZero R] {x : R}, x ≠ 0 → IsRadical x → Squarefree x
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp.sizeOf_spec : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : SizeOf R] (toFinsupp : AddMonoidAlgebra R ℕ),
  sizeOf { toFinsupp := toFinsupp } = 1 + sizeOf toFinsupp
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.flatten : Lean.IR.FnBody → Array Lean.IR.FnBody × Lean.IR.FnBody
-- Init.Data.Nat.Gcd
Nat.gcd_pow_right_of_gcd_eq_one : ∀ {k n m : ℕ}, n.gcd m = 1 → n.gcd (m ^ k) = 1
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.derivedLitsInvariant_performRupCheck : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n)
  (rupHints : Array ℕ) (f'_assignments_size : (f.performRupCheck rupHints).1.assignments.size = n),
  let rupCheckRes := f.performRupCheck rupHints;
  f.DerivedLitsInvariant f_assignments_size rupCheckRes.1.assignments f'_assignments_size rupCheckRes.2.1
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the smallest element that is greater than or equal to the
given element, returning `none` if no such element exists.
 -/
Std.TreeSet.getGE? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → Option α
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  (cc : CategoryTheory.Limits.CokernelCofork S.f) (hcc : CategoryTheory.Limits.IsColimit cc),
  (hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).H = 0
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addUnitIso_inv_app_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C)
  (X_1 : CategoryTheory.Discrete PUnit.{w + 1}),
  ((CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addUnitIso C).inv.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id
      (X.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1})))
-- Mathlib.Order.Filter.Lift
Filter.prod_lift'_lift' : ∀ {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} {f₁ : Filter α₁} {f₂ : Filter α₂}
  {g₁ : Set α₁ → Set β₁} {g₂ : Set α₂ → Set β₂},
  Monotone g₁ → Monotone g₂ → f₁.lift' g₁ ×ˢ f₂.lift' g₂ = f₁.lift fun s => f₂.lift' fun t => g₁ s ×ˢ g₂ t
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff_op : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂),
  Φ.IsLeftDerivabilityStructure ↔ Φ.op.IsRightDerivabilityStructure
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_range : ∀ {β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  {xs : Std.Legacy.Range} {init : β} {f : ℕ → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List ℕ) (cur : ℕ) (suff : List ℕ) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.Dynamics.Ergodic.Ergodic
PreErgodic.aeconst_set : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : autoParam (MeasureTheory.Measure α) PreErgodic._auto_1},
  PreErgodic f μ → ∀ ⦃s : Set α⦄, MeasurableSet s → f ⁻¹' s = s → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.Equiv.mk : ∀ {α : Type u} {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β},
  (Std.DHashMap.Internal.toListModel m₁.buckets).Perm (Std.DHashMap.Internal.toListModel m₂.buckets) → m₁.Equiv m₂
-- Batteries.Data.List.Basic
/-- Auxiliary for `modifyLast`: `modifyLast.go f l acc = acc.toList ++ modifyLast f l`.  -/
List.modifyLast.go : {α : Type u_1} → (α → α) → List α → Array α → List α
-- Mathlib.Topology.UniformSpace.Path
Path.instUniformSpace : {X : Type u_1} → [inst : UniformSpace X] → {x y : X} → UniformSpace (Path x y)
-- Init.Data.Vector.Lemmas
Vector.all_iff_forall : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.all p = true ↔ ∀ (i : ℕ) (x : i < n), p xs[i] = true
-- Std.Internal.Do.Triple.SpecLemmas
/-- The type of loop invariants used by the specifications of `for ... in ...` loops over strings.
A loop invariant is a function mapping the current position and state to a lattice element.
 -/
Std.Internal.Do.StringInvariant : String → Type u → Type u → Type u
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.card_cycleType_eq_one : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α}, σ.cycleType.card = 1 ↔ σ.IsCycle
-- Init.Data.OfScientific
/-- Precomputed values of `10 ^ e` for `0 ≤ e ≤ 22`. In this range, the values can be represented
exactly.
 -/
Float.exactlyRepresentablePowersOfTen : Array Float
-- Mathlib.NumberTheory.LSeries.PrimesInAP
_private.Mathlib.NumberTheory.LSeries.PrimesInAP.0.ArithmeticFunction.vonMangoldt.F''.eq_1 : ArithmeticFunction.vonMangoldt.F''✝ = ArithmeticFunction.vonMangoldt.F'✝ ∘ Prod.map id fun x => x + 1
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.isBase_iff_maximal_indep : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.IsBase B ↔ Maximal M.Indep B
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.killCompl_rename_app : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {f : σ → τ} (hf : Function.Injective f)
  (p : MvPolynomial σ R), (MvPolynomial.killCompl hf) ((MvPolynomial.rename f) p) = p
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_inter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β k},
      (m₁.inter m₂ ⋯).getD k fallback =
        if Std.DTreeMap.Internal.Impl.contains k m₂ = true then m₁.getD k fallback else fallback
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompHomotopyEquiv_comm₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃),
  CategoryTheory.CategoryStruct.comp
      (CochainComplex.mappingCone.inr
        (CochainComplex.mappingCone.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X₁)
          g ⋯))
      (CochainComplex.mappingConeCompHomotopyEquiv f g).inv =
    (CochainComplex.mappingConeCompTriangle f g).mor₂
-- Mathlib.Data.Finset.Range
Finset.subset_range : ∀ {s : Finset ℕ} {n : ℕ}, s ⊆ Finset.range n ↔ ∀ x ∈ s, x < n
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.t1Space_iff : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {N : Subgroup G},
  T1Space (G ⧸ N) ↔ IsClosed ↑N
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
SemiNormedGrp.instPreadditive : CategoryTheory.Preadditive SemiNormedGrp
-- Std.Data.ExtDHashMap.Basic
/-- Updates the values of the hash map by applying the given function to all mappings, keeping
only those mappings where the function returns `some` value.
 -/
Std.ExtDHashMap.filterMap : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} →
      {x : BEq α} →
        {x_1 : Hashable α} →
          [EquivBEq α] → [LawfulHashable α] → ((a : α) → β a → Option (γ a)) → Std.ExtDHashMap α β → Std.ExtDHashMap α γ
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Continuous.rpow_const : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ} {p : ℝ},
  Continuous f → (∀ (x : α), f x ≠ 0 ∨ 0 ≤ p) → Continuous fun x => f x ^ p
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The opposite of a binary biproduct data.  -/
CategoryTheory.Limits.BinaryBiproductData.op : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        CategoryTheory.Limits.BinaryBiproductData P Q →
          CategoryTheory.Limits.BinaryBiproductData (Opposite.op P) (Opposite.op Q)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Analytic
/-- If a function `R : 𝕜 → 𝕜` factors as `R z = (z - z₀) ^ (k + t) * R₁ z`, where `R₁` is
analytic everywhere, then there exists an everywhere analytic function `R₂ : 𝕜 → 𝕜` such that
the `k`-th iterated derivative of `R` is given by
`iteratedDeriv k R z = (z - z₀) ^ t * ((k + t)! / t ! * R₁ z + (z - z₀) * R₂ z)`.  -/
iteratedDeriv_mul_pow_sub_of_analytic : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CharZero 𝕜] [CompleteSpace 𝕜] {k t : ℕ} {z₀ : 𝕜} {R R₁ : 𝕜 → 𝕜},
  (∀ (z : 𝕜), AnalyticAt 𝕜 R₁ z) →
    (∀ (z : 𝕜), R z = (z - z₀) ^ (k + t) * R₁ z) →
      ∃ R₂,
        (∀ (z : 𝕜), AnalyticAt 𝕜 R₂ z) ∧
          ∀ (z : 𝕜), iteratedDeriv k R z = (z - z₀) ^ t * (↑(k + t).factorial / ↑t.factorial * R₁ z + (z - z₀) * R₂ z)
-- Mathlib.Algebra.Module.ULift
ULift.vaddLeft : {R : Type u} → {M : Type v} → [VAdd R M] → VAdd (ULift.{u_1, u} R) M
-- Mathlib.Geometry.Euclidean.MongePoint
_private.Mathlib.Geometry.Euclidean.MongePoint.0.Affine.Simplex.mongePointWeightsWithCircumcenter.match_1.eq_2 : ∀ (n : ℕ) (motive : Affine.Simplex.PointsWithCircumcenterIndex (n + 2) → Sort u_1)
  (h_1 : (a : Fin (n + 2 + 1)) → motive (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a))
  (h_2 : Unit → motive Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex),
  (match Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex with
    | Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a => h_1 a
    | Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex => h_2 ()) =
    h_2 ()
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.under_map_of_isPrimary_disjoint : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {I : Ideal R},
  I.IsPrimary → Disjoint ↑M ↑I → Ideal.under R (Ideal.map (algebraMap R S) I) = I