mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Minpoly.Basic
minpoly.subsingleton : ∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B) [Subsingleton B],
  minpoly A x = 1
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- Composition of morphisms in the indexing diagram for wide (co)equalizers.  -/
CategoryTheory.Limits.WalkingParallelFamily.Hom.comp : {J : Type w} →
  {X Y Z : CategoryTheory.Limits.WalkingParallelFamily J} →
    CategoryTheory.Limits.WalkingParallelFamily.Hom J X Y →
      CategoryTheory.Limits.WalkingParallelFamily.Hom J Y Z → CategoryTheory.Limits.WalkingParallelFamily.Hom J X Z
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.quotientMulEquiv.congr_simp : ∀ (G : Type u_1) (G' : Type u_2) [inst : Group G] [inst_1 : Group G'] (A : Type u_5) (B : Type u_6) (C : Type u_7)
  [inst_2 : CommRing A] [inst_3 : CommRing B] [inst_4 : CommRing C] [inst_5 : IsDomain C] [inst_6 : Algebra A B]
  [inst_7 : Algebra A C] [inst_8 : Algebra B C] [inst_9 : FaithfulSMul A B] [inst_10 : FaithfulSMul B C]
  [inst_11 : IsScalarTower A B C] [inst_12 : Finite G] [inst_13 : Finite G'] (N : Subgroup G) [inst_14 : N.Normal]
  [inst_15 : MulSemiringAction G C] [inst_16 : IsGaloisGroup G A C] [inst_17 : IsGaloisGroup (↥N) B C]
  [inst_18 : MulSemiringAction G' B] [inst_19 : IsGaloisGroup G' A B],
  IsGaloisGroup.quotientMulEquiv G G' A B C N = IsGaloisGroup.quotientMulEquiv G G' A B C N
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.injective_toPlots : ∀ {X : Type u_1}, Function.Injective DiffeologicalSpace.toPlots
-- Mathlib.Order.CompleteLattice.PiLex
_private.Mathlib.Order.CompleteLattice.PiLex.0.Pi.Lex.inf : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : LinearOrder ι] →
      [(i : ι) → CompleteLinearOrder (α i)] → [WellFoundedLT ι] → Set (Lex ((i : ι) → (fun i => α i) i)) → (i : ι) → α i
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.eqBoth.injEq : ∀ (gen gen_1 : Bool),
  (Lean.Meta.Grind.EMatchTheoremKind.eqBoth gen = Lean.Meta.Grind.EMatchTheoremKind.eqBoth gen_1) = (gen = gen_1)
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.coeff_subst_finite' : ∀ {R : Type u_2} [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S] {b : PowerSeries S},
  PowerSeries.HasSubst b →
    ∀ (f : PowerSeries R) (e : ℕ),
      Function.HasFiniteSupport fun d => (PowerSeries.coeff d) f • (PowerSeries.coeff e) (b ^ d)
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.instIsIsoFunctorLeftKanExtensionUnitOppositeTypeUliftYoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  (A : CategoryTheory.Functor C ℰ)
  [inst_2 : CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A],
  CategoryTheory.IsIso (CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.leftKanExtensionUnit A)
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.comap_liftQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (q : Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ f.ker),
  Submodule.comap (p.liftQ f h) q = Submodule.map p.mkQ (Submodule.comap f q)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RoiSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : SizeOf β]
  (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Roi α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mk₂_surjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.ComposableArrows C 2),
  ∃ X₀ X₁ X₂ f₀ f₁, X = CategoryTheory.ComposableArrows.mk₂ f₀ f₁
-- Mathlib.Topology.Algebra.Group.Basic
Subgroup.connectedComponentOfOne.eq_1 : ∀ (G : Type u_1) [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G],
  Subgroup.connectedComponentOfOne G = { carrier := connectedComponent 1, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.Data.FinEnum
FinEnum.instInt32 : FinEnum Int32
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.fromDFinsuppEquiv_symm_apply : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} [inst : DecidableEq ι]
  [inst_1 : Fintype ι] [inst_2 : CommSemiring R] [inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)]
  [inst_4 : (i : ι) → (k : κ i) → Module R (M i k)] {N : Type u_1} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  [inst_7 : (i : ι) → DecidableEq (κ i)] (f : MultilinearMap R (fun i => Π₀ (j : κ i), M i j) N) (p : (i : ι) → κ i),
  (MultilinearMap.fromDFinsuppEquiv κ R).symm f p = f.compLinearMap fun i => DFinsupp.lsingle (p i)
-- Mathlib.Algebra.Group.Defs
AddCommSemigroup.ext_iff : ∀ {G : Type u} {x y : AddCommSemigroup G}, x = y ↔ Add.add = Add.add
-- Mathlib.Analysis.Convolution
MeasureTheory.support_convolution_subset : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddCommGroup G],
  Function.support (MeasureTheory.convolution f g L μ) ⊆ Function.support f + Function.support g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.ordered_keys_toList : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → List.Pairwise (fun a b => compare a.1 b.1 = Ordering.lt) (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Init.Data.Order.Lemmas
Std.Total.rel_of_not_rel_swap : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Total r] {a b : α}, ¬r a b → r b a
-- Mathlib.Data.Nat.Factorization.PrimePow
Nat.Primes.prodNatEquiv_symm_apply : ∀ {n : ℕ} (hn : IsPrimePow n), Nat.Primes.prodNatEquiv.symm ⟨n, hn⟩ = (⟨n.minFac, ⋯⟩, n.factorization n.minFac - 1)
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
/-- An auxiliary lemma that is used to specialize the general divergence theorem to spaces that do
not have the form `Fin n → ℝ`.  -/
MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_of_equiv : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} {F : Type u_1}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : Preorder F]
  [inst_5 : MeasureTheory.MeasureSpace F] [BorelSpace F] (eL : F ≃L[ℝ] Fin (n + 1) → ℝ),
  (∀ (x y : F), eL x ≤ eL y ↔ x ≤ y) →
    MeasureTheory.MeasurePreserving (⇑eL) MeasureTheory.volume MeasureTheory.volume →
      ∀ (f : Fin (n + 1) → F → E) (f' : Fin (n + 1) → F → F →L[ℝ] E) (s : Set F),
        s.Countable →
          ∀ (a b : F),
            a ≤ b →
              (∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)) →
                (∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x) →
                  ∀ (DF : F → E),
                    (∀ (x : F), DF x = ∑ i, (f' i x) (eL.symm (Pi.single i 1))) →
                      MeasureTheory.IntegrableOn DF (Set.Icc a b) MeasureTheory.volume →
                        ∫ (x : F) in Set.Icc a b, DF x =
                          ∑ i,
                            ((∫ (x : Fin n → ℝ) in Set.Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove),
                                f i (eL.symm (i.insertNth (eL b i) x))) -
                              ∫ (x : Fin n → ℝ) in Set.Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove),
                                f i (eL.symm (i.insertNth (eL a i) x)))
-- Mathlib.Analysis.Normed.Group.Hom
/-- If a bounded group homomorphism map is constructed from a group homomorphism
via the constructor `AddMonoidHom.mkNormedAddGroupHom`, then its norm is bounded by the bound
given to the constructor or zero if this bound is negative.  -/
NormedAddGroupHom.mkNormedAddGroupHom_norm_le' : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] (f : V₁ →+ V₂)
  {C : ℝ} (h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖), ‖f.mkNormedAddGroupHom C h‖ ≤ max C 0
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.modify.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α × RBTree.RBNode.Path α → Sort u_2) →
    (x : RBTree.RBNode α × RBTree.RBNode.Path α) →
      ((snd : RBTree.RBNode.Path α) → motive (RBTree.RBNode.nil, snd)) →
        ((c : RBTree.RBColor) →
            (a : RBTree.RBNode α) →
              (x : α) →
                (b : RBTree.RBNode α) → (path : RBTree.RBNode.Path α) → motive (RBTree.RBNode.node c a x b, path)) →
          motive x
-- Lean.Meta.Match.SimpH
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.State.eqsNew : Lean.Meta.Match.SimpH.State✝ → List Lean.FVarId
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.regular : Lean.Elab.Term.Do.ToTerm.Kind
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_congr_set : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s t : Set 𝕜},
  s =ᶠ[nhds x] t → (HasDerivWithinAt f f' s x ↔ HasDerivWithinAt f f' t x)
-- Mathlib.Order.RelSeries
RelSeries.snoc.eq_1 : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newLast : α) (rel : (p.last, newLast) ∈ r),
  p.snoc newLast rel = p.append (RelSeries.singleton r newLast) rel
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ : S₁ ⟶ S₂} →
          (h₀ : S₁.X₁ ⟶ S₂.X₁) →
            autoParam (CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0)
                CategoryTheory.ShortComplex.Homotopy.h₀_f._autoParam →
              (h₁ : S₁.X₂ ⟶ S₂.X₁) →
                (h₂ : S₁.X₃ ⟶ S₂.X₂) →
                  (h₃ : S₁.X₃ ⟶ S₂.X₃) →
                    autoParam (CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0)
                        CategoryTheory.ShortComplex.Homotopy.g_h₃._autoParam →
                      autoParam (φ₁.τ₁ = CategoryTheory.CategoryStruct.comp S₁.f h₁ + h₀ + φ₂.τ₁)
                          CategoryTheory.ShortComplex.Homotopy.comm₁._autoParam →
                        autoParam
                            (φ₁.τ₂ =
                              CategoryTheory.CategoryStruct.comp S₁.g h₂ + CategoryTheory.CategoryStruct.comp h₁ S₂.f +
                                φ₂.τ₂)
                            CategoryTheory.ShortComplex.Homotopy.comm₂._autoParam →
                          autoParam (φ₁.τ₃ = h₃ + CategoryTheory.CategoryStruct.comp h₂ S₂.g + φ₂.τ₃)
                              CategoryTheory.ShortComplex.Homotopy.comm₃._autoParam →
                            CategoryTheory.ShortComplex.Homotopy φ₁ φ₂
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vaddCommClass_set' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α γ] [inst_1 : VAdd β γ] [VAddCommClass α β γ],
  VAddCommClass α (Set β) (Set γ)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.instAddCommGroup : {R : Type u} →
  [inst : CommRing R] →
    {M : Type u_1} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {N : Type u_2} → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → AddCommGroup (M →ₚₗ[R] N)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.coprod.eq_1 : ∀ {A : Type u_2} {B : Type u_3} {E : Type u_6} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [inst_4 : CommMonoid E] [inst_5 : TopologicalSpace E] [inst_6 : ContinuousMul E]
  (f : A →ₜ* E) (g : B →ₜ* E), f.coprod g = (ContinuousMonoidHom.mul E).comp (f.prodMap g)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- The variation of a function on `Iic a` is the sum of the variation on `Iio a` and the
contribution of `a`, i.e., the distance between the left limit and the value at `a`.
We give a version relative to a set `s`.  -/
eVariationOn.eVariationOn_on_inter_Iic_eq_Iio_add_edist : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α} {a : α} {l : E},
  (nhdsWithin a (s ∩ Set.Iio a)).NeBot →
    a ∈ s →
      Filter.Tendsto f (nhdsWithin a (s ∩ Set.Iio a)) (nhds l) →
        eVariationOn f (s ∩ Set.Iic a) = eVariationOn f (s ∩ Set.Iio a) + edist (f a) l
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquivLast.eq_1 : ∀ {n : ℕ}, finSuccEquivLast = finSuccEquiv' (Fin.last n)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- Continuous linear map sending a function of `Lp F p μ` to the same function in
`Lp F p (μ.restrict s)`.  -/
MeasureTheory.LpToLpRestrictCLM : (X : Type u_1) →
  (F : Type u_4) →
    {mX : MeasurableSpace X} →
      (𝕜 : Type u_5) →
        [inst : NormedRing 𝕜] →
          [inst_1 : NormedAddCommGroup F] →
            [inst_2 : Module 𝕜 F] →
              [inst_3 : IsBoundedSMul 𝕜 F] →
                (μ : MeasureTheory.Measure X) →
                  (p : ENNReal) →
                    [hp : Fact (1 ≤ p)] →
                      (s : Set X) → ↥(MeasureTheory.Lp F p μ) →L[𝕜] ↥(MeasureTheory.Lp F p (μ.restrict s))
-- Mathlib.CategoryTheory.Sites.LeftExact
/-- Auxiliary definition for `liftToDiagramLimitObj`.  -/
CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux : {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] →
                  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape K D] →
                    {W : (J.Cover X)ᵒᵖ} →
                      (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) →
                        (E :
                            CategoryTheory.Limits.Cone
                              (F.comp
                                ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj W)))) →
                          (i : (Opposite.unop W).Arrow) → E.pt ⟶ (CategoryTheory.Limits.limit F).obj (Opposite.op i.Y)
-- Mathlib.Algebra.Group.Ideal
AddSemigroupIdeal.mem_closure : ∀ {M : Type u_1} [inst : Add M] {s : Set M} {x : M},
  x ∈ AddSemigroupIdeal.closure s ↔ ∀ (p : AddSemigroupIdeal M), s ⊆ ↑p → x ∈ p
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α} (h : t.WF)
  {h' : k ∈ Std.DTreeMap.Internal.Impl.filter! f t}, (Std.DTreeMap.Internal.Impl.filter! f t).get k h' = t.get k ⋯
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Compose a `0`-hypercover with a morphism on the right.  -/
CategoryTheory.Precoverage.ZeroHypercover.pushforward : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      [J.IsStableUnderComposition] →
        [J.HasIsos] →
          {X Y : C} →
            (f : X ⟶ Y) → CategoryTheory.Presieve.singleton f ∈ J.coverings Y → J.ZeroHypercover X → J.ZeroHypercover Y
-- Mathlib.Analysis.MeanInequalities
Real.geom_mean_eq_arith_mean2_weighted_iff_of_pos : ∀ {w₁ w₂ p₁ p₂ : ℝ}, 0 < w₁ → 0 < w₂ → 0 ≤ p₁ → 0 ≤ p₂ → w₁ + w₂ = 1 → (p₁ ^ w₁ * p₂ ^ w₂ = w₁ * p₁ + w₂ * p₂ ↔ p₁ = p₂)
-- Init.Data.Array.Lemmas
Array.getElem_swap : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ} (hi : i < xs.size) (hj : j < xs.size) {k : ℕ}
  (hk : k < (xs.swap i j hi hj).size), (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)},
  (m.alter k f).size =
    if k ∈ m ∧ (f (m.get? k)).isNone = true then m.size - 1
    else if k ∉ m ∧ (f (m.get? k)).isSome = true then m.size + 1 else m.size
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_snd_coe : ∀ (k : ℕ) (x : Fin k → ℕ) (a : Fin k), ↑((Finset.Nat.sigmaAntidiagonalTupleEquivTuple k).symm x).snd a = x a
-- Mathlib.Analysis.Asymptotics.TVS
/-- `f =o[𝕜; l] g` (`IsLittleOTVS 𝕜 l f g`) is a generalization of `f =o[l] g` (`IsLittleO l f g`)
that works in topological `𝕜`-vector spaces.

Given two functions `f` and `g` taking values in topological vector spaces
over a normed field `K`,
we say that $f = o(g)$ if for any neighborhood of zero `U` in the codomain of `f`
there exists a neighborhood of zero `V` in the codomain of `g`
such that $\operatorname{gauge}_{K, U} (f(x)) = o(\operatorname{gauge}_{K, V} (g(x)))$,
where $\operatorname{gauge}_{K, U}(y) = \inf \{‖c‖ \mid y ∈ c • U\}$.

We use an `ENNReal`-valued function `egauge` for the gauge,
so we unfold the definition of little o instead of reusing it.  -/
Asymptotics.IsLittleOTVS : (𝕜 : Type u_1) →
  {α : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        [ENorm 𝕜] →
          [TopologicalSpace E] →
            [TopologicalSpace F] → [Zero E] → [Zero F] → [SMul 𝕜 E] → [SMul 𝕜 F] → Filter α → (α → E) → (α → F) → Prop
-- Mathlib.Order.SuccPred.Basic
Order.succ_injective : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α], Function.Injective Order.succ
-- Mathlib.Data.Complex.Basic
/-- A real segment `[a₁, a₂]` translated by `b * I` is the complex line segment.  -/
Complex.horizontalSegment_eq : ∀ (a₁ a₂ b : ℝ), (fun x => ↑x + ↑b * Complex.I) '' Set.uIcc a₁ a₂ = Set.uIcc a₁ a₂ ×ℂ {b}
-- Std.Time.Date.Unit.Day
/-- `Ordinal` represents a bounded value for days, which ranges between 1 and 31.
 -/
Std.Time.Day.Ordinal : Type
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryLE_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h' : ∃ a ∈ t₁, (cmp a k).isLE = true} (h : t₁.Equiv t₂), t₁.getEntryLE k h' = t₂.getEntryLE k ⋯
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- Transport a submersive presentation along an algebra isomorphism.  -/
Algebra.SubmersivePresentation.ofAlgEquiv : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] →
                Algebra.SubmersivePresentation R S ι σ →
                  {T : Type u_1} →
                    [inst_4 : CommRing T] →
                      [inst_5 : Algebra R T] → (S ≃ₐ[R] T) → Algebra.SubmersivePresentation R T ι σ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.keysArray_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {f : α → β → γ},
  (Std.TreeMap.map f t).keysArray = t.keysArray
-- Mathlib.Algebra.Quaternion
Quaternion.sub_re_self : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), a - ↑a.re = a.im
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toEquiv : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A ≃ₐ[R] B) → A ≃ B
-- Mathlib.Order.PrimeIdeal
Order.Ideal.IsPrime.mem_or_compl_mem : ∀ {P : Type u_1} [inst : BooleanAlgebra P] {x : P} {I : Order.Ideal P}, I.IsPrime → x ∈ I ∨ xᶜ ∈ I
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.isRelPrime_iff_no_prime_factors : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b : R},
  a ≠ 0 → (IsRelPrime a b ↔ ∀ ⦃d : R⦄, d ∣ a → d ∣ b → ¬Prime d)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.unit : {C : Type u} → CategoryTheory.FreeMonoidalCategory C
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiffTag.change : Lean.Widget.ExprDiffTag✝
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z) (s : CategoryTheory.Limits.PullbackCone f g),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f g s)
      (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f g).fst =
    s.fst
-- Mathlib.Algebra.Ring.Commute
sq_eq_sq_iff_eq_or_eq_neg : ∀ {R : Type u} [inst : CommRing R] [NoZeroDivisors R] {a b : R}, a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_natDegree_le : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), f.eraseLead.natDegree ≤ f.natDegree - 1
-- Std.Sync.Channel
/-- Creates a `Selector` that resolves once `ch` has data available and provides that data.
In particular if `ch` is closed while waiting on this `Selector` and no data is available already
this will resolve to `none`.
 -/
Std.CloseableChannel.recvSelector : {α : Type} → Std.CloseableChannel α → Std.Async.Selector (Option α)
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Shrinking does nothing for the same universe level.  -/
CategoryTheory.Sieve.shrinkFunctorIsoFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → (S : CategoryTheory.Sieve X) → (CategoryTheory.Sieve.shrinkFunctor.{v₁, v₁, u₁} S).toFunctor ≅ S.functor
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.var.sizeOf_spec : ∀ (i : Nat.Internal.Linear.Var), sizeOf (Nat.Internal.Linear.Expr.var i) = 1 + sizeOf i
-- Mathlib.Algebra.GroupWithZero.Action.Units
smul_inv_smul₀ : ∀ {α : Type u_4} {β : Type u_5} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
  a ≠ 0 → ∀ (x : β), a • a⁻¹ • x = x
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_add_add_eq_append : ∀ {m n k : ℕ}, (m<...=m + n + k).toList = (m<...=m + n).toList ++ ((m + n)<...=m + n + k).toList
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for `Nat.ascFactorial`.  -/
Mathlib.Meta.Positivity.evalAscFactorial : Mathlib.Meta.Positivity.PositivityExt
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.valuesArray_eq_toArray_map : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.valuesArray = (List.map (fun x => x.snd) t.toListModel).toArray
-- Mathlib.Topology.Gluing
/-- The gluing of an open cover is homeomorphic to the original space.  -/
TopCat.GlueData.openCoverGlueHomeo : {α : Type u} →
  [inst : TopologicalSpace α] →
    {J : Type u} →
      (U : J → TopologicalSpace.Opens α) → ⋃ i, ↑(U i) = Set.univ → ↑(TopCat.GlueData.ofOpenSubsets U).glued ≃ₜ α
-- Std.Data.DHashMap.Iterator
/-- Returns a finite iterator over the keys of a dependent hash map.
The iterator yields the keys in order and then terminates.

The key and value types must live in the same universe.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.DHashMap.keysIter : {α : Type u} → {β : α → Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Std.DHashMap α β → Std.Iter α
-- Mathlib.Data.EReal.Inv
EReal.le_iff_sign : ∀ {x y : EReal},
  x ≤ y ↔
    SignType.sign x < SignType.sign y ∨
      SignType.sign x = SignType.neg ∧ SignType.sign y = SignType.neg ∧ y.abs ≤ x.abs ∨
        SignType.sign x = SignType.zero ∧ SignType.sign y = SignType.zero ∨
          SignType.sign x = SignType.pos ∧ SignType.sign y = SignType.pos ∧ x.abs ≤ y.abs