mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Cardinal.Finite
Cardinal.natCast_eq_toENat_iff : ∀ {n : ℕ} {c : Cardinal.{u_3}}, ↑n = Cardinal.toENat c ↔ ↑n = c
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.id_apply : ∀ {α : Type u_2} [inst : NonUnitalNonAssocSemiring α] (x : α), (NonUnitalRingHom.id α) x = x
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_hom_comp_biproduct_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (X : C) (f : J → C) (j : J)
  {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)) h
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.centerToMulOpposite_symm_apply_coe : ∀ (G : Type u_1) [inst : Group G] (r : ↥(Subsemigroup.center Gᵐᵒᵖ)),
  ↑((Subgroup.centerToMulOpposite G).symm r) = MulOpposite.unop ↑r
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.map_units : ∀ {R : Type u_1} {inst : CommSemiring R} {M : Type u_2} {M' : Type u_3} {inst_1 : AddCommMonoid M}
  {inst_2 : AddCommMonoid M'} {inst_3 : Module R M} {inst_4 : Module R M'} {S : Submonoid R} (f : M →ₗ[R] M')
  [self : IsLocalizedModule S f] (x : ↥S), IsUnit ((algebraMap R (Module.End R M')) ↑x)
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the smallest key in the tree map, returning `fallback` if the tree map is empty.
 -/
Std.TreeMap.Raw.minKeyD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → α
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.reduce.eq_1 : ∀ {m : ℤ} (A : FixedDetMatrix (Fin 2) ℤ m),
  FixedDetMatrices.reduce A =
    if ↑A 1 0 = 0 then
      if 0 < ↑A 0 0 then ModularGroup.T ^ (-(↑A 0 1 / ↑A 1 1)) • A
      else ModularGroup.T ^ (-(-↑A 0 1 / -↑A 1 1)) • ModularGroup.S • ModularGroup.S • A
    else FixedDetMatrices.reduce (FixedDetMatrices.reduceStep A)
-- Mathlib.Topology.Algebra.Algebra
Subalgebra.topologicalClosure_map : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : IsSemitopologicalSemiring A] [inst_8 : IsSemitopologicalSemiring B] (f : A →A[R] B),
  IsClosedMap ⇑f →
    ∀ (s : Subalgebra R A), (Subalgebra.map (↑f) s).topologicalClosure = Subalgebra.map (↑f) s.topologicalClosure
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.faceSingletonComplIso_hom_ι_assoc : ∀ {n : ℕ} (i : Fin (n + 2)) {Z : SSet} (h : SSet.stdSimplex.obj { len := n + 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso i).hom
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.face {i}ᶜ).ι h) =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i) h
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.one_lt_rpow : ∀ {x : ENNReal} {z : ℝ}, 1 < x → 0 < z → 1 < x ^ z
-- Mathlib.Order.InitialSeg
InitialSeg.coe_toOrderEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α ≤i β), ⇑f.toOrderEmbedding = ⇑f
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.getFType : Lean.Elab.Tactic.ElimApp.M✝ Lean.Expr
-- Mathlib.Algebra.Group.Defs
AddMonoid.toAddSemigroup : {M : Type u} → [self : AddMonoid M] → AddSemigroup M
-- Init.Data.Array.Erase
Array.erase_eq_self_iff : ∀ {α : Type u_1} [inst : BEq α] {a : α} [LawfulBEq α] {xs : Array α}, xs.erase a = xs ↔ a ∉ xs
-- Mathlib.Data.QPF.Multivariate.Constructions.Prj
/-- Abstraction function of the `QPF` instance  -/
MvQPF.Prj.abs : {n : ℕ} → (i : Fin2 n) → ⦃α : TypeVec.{u_1} n⦄ → ↑(MvQPF.Prj.P i) α → MvQPF.Prj i α
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.ext' : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e e' : Bundle.Trivialization F proj),
  e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph → e.baseSet = e'.baseSet → e = e'
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.Functor.essImage_ext_iff : ∀ {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 Y : F.EssImageSubcategory} {f g : X ⟶ Y},
  f = g ↔ F.essImage.ι.map f = F.essImage.ι.map g
-- Mathlib.RingTheory.Filtration
/-- The `R[IX]`-submodule of `M[X]` associated with an `I`-filtration.  -/
Ideal.Filtration.submodule : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {I : Ideal R} → I.Filtration M → Submodule (↥(reesAlgebra I)) (PolynomialModule R M)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.elabModSnippet' : Lean.DeclarationRange → ℕ → Lean.TSyntaxArray `block → Lean.Doc.DocM Lean.VersoModuleDocs.Snippet
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- If the point passed to `secondInter` is a vertex of a simplex, lying on the sphere, and all
vertices lie on or inside the sphere, and the vector passed to `secondInter` is given by a
subtraction involving that vertex and a point in the interior of the simplex, the given vertex
and the result of `secondInter` are on opposite sides of the face opposite that vertex.  -/
EuclideanGeometry.Sphere.sOppSide_faceOpposite_secondInter_of_mem_interior : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {n : ℕ} [inst_4 : n.AtLeastTwo]
  {sx : Affine.Simplex ℝ P n} {i : Fin (n + 1)},
  sx.points i ∈ s →
    (∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius) →
      ∀ {p : P},
        p ∈ sx.interior →
          (affineSpan ℝ (Set.range (sx.faceOpposite i).points)).SOppSide (sx.points i)
            (s.secondInter (sx.points i) (p -ᵥ sx.points i))
-- Init.Data.Vector.Basic
Vector.instBEq : {α : Type u_1} → {n : ℕ} → [BEq α] → BEq (Vector α n)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.orElse_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {x : OptionT m α} {h : Unit → OptionT m α} [inst : Monad m]
  [inst_1 : Std.Do.WPMonad m ps] (Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)),
  ⦃(Std.Do.wp x).apply (Q.1, fun x => (Std.Do.wp (h ())).apply Q, Q.2.2)⦄ OrElse.orElse x h ⦃Q⦄
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv_eq_none : ∀ {n : ℕ} {i : Fin (n + 1)}, (finSuccEquiv n) i = none ↔ i = 0
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_rpow_nnreal : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a : A} {x : NNReal},
  CFC.sqrt (a ^ ↑x) = a ^ (↑x / 2)
-- Std.Http.Data.Chunk
/-- The proof that it's a valid extension value.
 -/
Std.Http.Chunk.ExtensionValue.isValidExtensionValue : ∀ (self : Std.Http.Chunk.ExtensionValue), Std.Http.Chunk.IsValidExtensionValue self.value
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.IsUniversal.hom_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal) {c : C}
  (η : f.right ⟶ c), η = h.desc (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f.hom (T.map η)))
-- Mathlib.Algebra.Group.Submonoid.Saturation
/-- If `M` is commutative, we only need to check the right condition `y ∈ s`.  -/
Submonoid.MulSaturated.of_right : ∀ {M : Type u_2} [inst : CommMonoid M] {s : Submonoid M}, (∀ ⦃x y : M⦄, x * y ∈ s → y ∈ s) → s.MulSaturated
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instSMul : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] →
            [inst_4 : IsScalarTower 𝕜 A A] →
              {S : Type u_3} →
                [inst_5 : Monoid S] →
                  [inst_6 : DistribMulAction S A] →
                    [SMulCommClass 𝕜 S A] →
                      [ContinuousConstSMul S A] →
                        [IsScalarTower S A A] → [SMulCommClass S A A] → SMul S (DoubleCentralizer 𝕜 A)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β},
  (t.alter k f).getKey? k' =
    if cmp k k' = Ordering.eq then if (f t[k]?).isSome = true then some k else none else t.getKey? k'
-- Mathlib.Data.Fin.Parity
Fin.odd_of_val : ∀ {n : ℕ} {k : Fin n} [inst : NeZero n], Odd ↑k → Odd k
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.getAppRevArgsAux : Lean.Expr → Array Lean.Expr → Array Lean.Expr
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
/-- Given a point `Φ` on a site `(C, J)`, and an object `M` of a category `A`,
this is the skyscraper presheaf with value `M`: it sends `X : C` to the
product of copies of `M` indexed by `Φ.fiber.obj X`.  -/
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      J.Point →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [CategoryTheory.Limits.HasProducts A] → A → CategoryTheory.Functor Cᵒᵖ A
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.instAddZeroClass : {R : Type u_1} → [inst : LinearOrder R] → [inst_1 : TopologicalSpace R] → AddZeroClass (StieltjesFunction R)
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `upperSemicontinuousOn_inv_iff`. -/
LowerSemicontinuousOn.inv : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} [inst_1 : PartialOrder β]
  [inst_2 : CommGroup β] [IsOrderedMonoid β], LowerSemicontinuousOn f s → UpperSemicontinuousOn f⁻¹ s
-- Mathlib.RingTheory.AdicCompletion.Topology
IsAdicComplete.congr_ringEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (I : Ideal R) (e : R ≃+* S),
  IsAdicComplete (Ideal.map e I) S ↔ IsAdicComplete I R
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.CallHierarchy : Type
-- Mathlib.GroupTheory.NoncommPiCoprod
AddMonoidHom.noncommPiCoprod_apply : ∀ {M : Type u_1} [inst : AddMonoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → AddMonoid (N i)] (ϕ : (i : ι) → N i →+ M)
  {hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)} (h : (i : ι) → N i),
  (AddMonoidHom.noncommPiCoprod ϕ hcomm) h = Finset.univ.noncommSum (fun i => (ϕ i) (h i)) ⋯
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.comap_eq_ker : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {H : AddSubgroup N},
  AddSubgroup.comap f H = f.ker ↔ Disjoint H f.range
-- Mathlib.Computability.NFA
NFA.append_preimage_acceptsFrom : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) {S : Set σ} {x : List α},
  (fun x_1 => x ++ x_1) ⁻¹' M.acceptsFrom S = M.acceptsFrom (M.evalFrom S x)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- A function is `C^n` at a point, for `n : ℕ`, if and only if it is `C^n` on
a neighborhood of this point.  -/
contMDiffAt_iff_contMDiffOn_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {n : WithTop ℕ∞}
  [IsManifold I n M] [IsManifold I' n M'], n ≠ ↑⊤ → (ContMDiffAt I I' n f x ↔ ∃ u ∈ nhds x, ContMDiffOn I I' n f u)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
multipliable_of_hasFiniteMulSupport : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {L : SummationFilter β}
  [L.HasSupport], Function.HasFiniteMulSupport f → Multipliable f L
-- Mathlib.AlgebraicTopology.MooreComplex
AlgebraicTopology.NormalizedMooreComplex.objX_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (X : CategoryTheory.SimplicialObject C), AlgebraicTopology.NormalizedMooreComplex.objX X 0 = ⊤
-- Mathlib.MeasureTheory.Function.LpSeminorm.Trim
MeasureTheory.essSup_trim : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → ENNReal},
  Measurable f → essSup f (μ.trim hm) = essSup f μ
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- A seminorm on an additive group `G` is a function `f : G → ℝ` that preserves zero, is
subadditive and such that `f (-x) = f x` for all `x`.  -/
AddGroupSeminorm : (G : Type u_6) → [AddGroup G] → Type u_6
-- Mathlib.Analysis.InnerProductSpace.Calculus
DifferentiableOn.inner : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {G : Type u_4} [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {f g : G → E}
  {s : Set G}, DifferentiableOn ℝ f s → DifferentiableOn ℝ g s → DifferentiableOn ℝ (fun x => inner 𝕜 (f x) (g x)) s
-- Init.Data.List.Lex
List.lex_eq_false_iff_ge : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] [inst_2 : LT α] [inst_3 : DecidableLT α] {l₁ l₂ : List α},
  (l₁.lex l₂ fun x1 x2 => decide (x1 < x2)) = false ↔ l₂ ≤ l₁
-- Mathlib.Data.Num.Lemmas
Num.bit1_of_bit1 : ∀ (n : Num), n + n + 1 = n.bit1
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofPartialTermInfo.inj : ∀ {i i_1 : Lean.Elab.PartialTermInfo},
  Lean.Elab.Info.ofPartialTermInfo i = Lean.Elab.Info.ofPartialTermInfo i_1 → i = i_1
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.comm' : ∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_3} (F : FormalGroup R) [F.IsComm] {f g : MvPowerSeries σ R},
  PowerSeries.HasSubst f →
    PowerSeries.HasSubst g → MvPowerSeries.subst ![f, g] F.toPowerSeries = MvPowerSeries.subst ![g, f] F.toPowerSeries
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.ShortExact.map_of_exact : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    ∀ (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms]
      [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F],
      (S.map F).ShortExact
-- Aesop.Stats.Report
Aesop.StatsReport.scriptsNontrivial : Aesop.StatsReport
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.inj₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)}
  [self : SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] ⦃a : α⦄ ⦃b : β⦄ ⦃c c' : γ⦄,
  (a, b, c) ∈ t → (a, b, c') ∈ t → c = c'
-- Mathlib.Algebra.Group.Equiv.Opposite
AddMonoidHom.fromOpposite_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N)
  (hf : ∀ (x y : M), AddCommute (f x) (f y)), ⇑(f.fromOpposite hf) = ⇑f ∘ AddOpposite.unop
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- Multiseries representing `basis[n]`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial : (basis : Tactic.ComputeAsymptotics.Basis) → ℕ → Tactic.ComputeAsymptotics.MultiseriesExpansion basis
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.interface : Lean.Lsp.SemanticTokenType
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_nat_atTop_induction_of_eventually_pos : ∀ {f g : ℕ → ℝ},
  (∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ f n) →
    (∀ᶠ (n : ℕ) in Filter.atTop, 0 < g n) →
      (∀ᶠ (n₀ : ℕ) in Filter.atTop,
          ∃ C₀, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n) →
        f =O[Filter.atTop] g
-- Mathlib.Data.ENat.Basic
ENat.lift_le_iff : ∀ {x : ℕ∞} {h : x < ⊤} {n : ℕ}, x.lift h ≤ n ↔ x ≤ ↑n
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.mk.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (binderName : Lean.Name)
  (params : Array (Lean.Compiler.LCNF.Param pu)) (type : Lean.Expr) (value : Lean.Compiler.LCNF.Code pu)
  (fvarId_1 : Lean.FVarId) (binderName_1 : Lean.Name) (params_1 : Array (Lean.Compiler.LCNF.Param pu))
  (type_1 : Lean.Expr) (value_1 : Lean.Compiler.LCNF.Code pu),
  (Lean.Compiler.LCNF.FunDecl.mk fvarId binderName params type value =
      Lean.Compiler.LCNF.FunDecl.mk fvarId_1 binderName_1 params_1 type_1 value_1) =
    (fvarId = fvarId_1 ∧ binderName = binderName_1 ∧ params = params_1 ∧ type = type_1 ∧ value = value_1)
-- Lean.Elab.BuiltinNotation
/-- Return syntax `MProd.mk elems[0] (MProd.mk elems[1] ... (MProd.mk elems[elems.size - 2] elems[elems.size - 1])))`  -/
Lean.Elab.Term.mkMPairs : Array Lean.Term → Lean.MacroM Lean.Term
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.IsHomological.exact : ∀ {C : Type u_1} {A : Type u_3} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.HasShift C ℤ}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} A} {F : CategoryTheory.Functor C A}
  {inst_3 : CategoryTheory.Limits.HasZeroObject C} {inst_4 : CategoryTheory.Preadditive C}
  {inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_6 : CategoryTheory.Pretriangulated C}
  {inst_7 : CategoryTheory.Abelian A} [self : F.IsHomological] (T : CategoryTheory.Pretriangulated.Triangle C)
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).map F).Exact
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.H2π_comp_map_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↥(groupCohomology.cocycles₂ A)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.map f φ 2))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π A)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π B))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.mapCocycles₂ f φ)) x)
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α} {h₁ : a ∈ m.insert k}, (m.insert k).get a h₁ = if h₂ : (k == a) = true ∧ k ∉ m then k else m.get a ⋯
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.Pair.mk.inj : ∀ {ι : Type u_1} {M : ι → Type u_2} {inst : (i : ι) → Monoid (M i)} {i : ι} {head : M i} {tail : Monoid.CoprodI.Word M}
  {fstIdx_ne : tail.fstIdx ≠ some i} {head_1 : M i} {tail_1 : Monoid.CoprodI.Word M}
  {fstIdx_ne_1 : tail_1.fstIdx ≠ some i},
  { head := head, tail := tail, fstIdx_ne := fstIdx_ne } =
      { head := head_1, tail := tail_1, fstIdx_ne := fstIdx_ne_1 } →
    head = head_1 ∧ tail = tail_1
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Around each point, there are only finitely many nonzero functions in the family.  -/
SmoothPartitionOfUnity.locallyFinite' : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : optParam (Set M) Set.univ} (self : SmoothPartitionOfUnity ι I M s),
  LocallyFinite fun i => Function.support ⇑(self.toFun i)
-- Mathlib.Analysis.SpecificLimits.Normed
/-- If `‖f n‖ ≤ C * r ^ n` for all `n : ℕ` and some `r < 1`, then the partial sums of `f` form a
Cauchy sequence. This lemma does not assume `0 ≤ r` or `0 ≤ C`.  -/
cauchySeq_finset_of_geometric_bound : ∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] {r C : ℝ} {f : ℕ → α},
  r < 1 → (∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n) → CauchySeq fun s => ∑ x ∈ s, f x
-- Mathlib.Order.Category.BddDistLat
BddDistLat.ext_iff : ∀ {X Y : BddDistLat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X.toDistLat), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.getConfig : Lean.Meta.Sym.Simp.SimpM Lean.Meta.Sym.Simp.Config
-- Lean.Meta.Tactic.Congr
/-- Try to apply `implies_congr`.
 -/
Lean.MVarId.congrImplies? : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Init.Data.List.MinMaxOn
List.minOn?_mem : ∀ {β : Type u_1} {α : Type u_2} {a : α} [inst : LE β] [inst_1 : DecidableLE β] {xs : List α} {f : α → β},
  List.minOn? f xs = some a → a ∈ xs
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.norm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : (NumberField.RingOfIntegers K)ˣ),
  |(Algebra.norm ℚ) ((algebraMap (NumberField.RingOfIntegers K) K) ↑x)| = 1
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.edgeFinset_sup : ∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V} [inst : Fintype ↑G₁.edgeSet] [inst_1 : Fintype ↑G₂.edgeSet]
  [inst_2 : Fintype ↑(G₁ ⊔ G₂).edgeSet] [inst_3 : DecidableEq V], (G₁ ⊔ G₂).edgeFinset = G₁.edgeFinset ∪ G₂.edgeFinset
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  {φQ : h₁.Q ⟶ h₂.Q} {φH : h₁.H ⟶ h₂.H}
  {commp :
    autoParam (CategoryTheory.CategoryStruct.comp h₁.p φQ = CategoryTheory.CategoryStruct.comp φ.τ₂ h₂.p)
      CategoryTheory.ShortComplex.RightHomologyMapData.commp._autoParam}
  {commg' :
    autoParam (CategoryTheory.CategoryStruct.comp φQ h₂.g' = CategoryTheory.CategoryStruct.comp h₁.g' φ.τ₃)
      CategoryTheory.ShortComplex.RightHomologyMapData.commg'._autoParam}
  {commι :
    autoParam (CategoryTheory.CategoryStruct.comp φH h₂.ι = CategoryTheory.CategoryStruct.comp h₁.ι φQ)
      CategoryTheory.ShortComplex.RightHomologyMapData.commι._autoParam}
  {φQ_1 : h₁.Q ⟶ h₂.Q} {φH_1 : h₁.H ⟶ h₂.H}
  {commp_1 :
    autoParam (CategoryTheory.CategoryStruct.comp h₁.p φQ_1 = CategoryTheory.CategoryStruct.comp φ.τ₂ h₂.p)
      CategoryTheory.ShortComplex.RightHomologyMapData.commp._autoParam}
  {commg'_1 :
    autoParam (CategoryTheory.CategoryStruct.comp φQ_1 h₂.g' = CategoryTheory.CategoryStruct.comp h₁.g' φ.τ₃)
      CategoryTheory.ShortComplex.RightHomologyMapData.commg'._autoParam}
  {commι_1 :
    autoParam (CategoryTheory.CategoryStruct.comp φH_1 h₂.ι = CategoryTheory.CategoryStruct.comp h₁.ι φQ_1)
      CategoryTheory.ShortComplex.RightHomologyMapData.commι._autoParam},
  { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι } =
      { φQ := φQ_1, φH := φH_1, commp := commp_1, commg' := commg'_1, commι := commι_1 } →
    φQ = φQ_1 ∧ φH = φH_1
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [inst_2 : Inhabited α] [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ \ m₂).get! k = default