mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable,
then $[E:F] [K:E]_i = [K:F]_i$.
It is a special case of `Field.lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic`, and is an
intermediate result used to prove it.  -/
Field.lift_rank_mul_lift_insepDegree_of_isPurelyInseparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F E],
  Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (Field.insepDegree E K) =
    Cardinal.lift.{v, w} (Field.insepDegree F K)
-- Init.Data.Vector.Lex
Vector.le_of_lt : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [i : Std.Asymm fun x1 x2 => x1 < x2] {xs ys : Vector α n}, xs < ys → xs ≤ ys
-- Mathlib.Algebra.Order.Ring.Cone
RingConeClass.mk : ∀ {S : Type u_1} {R : outParam (Type u_2)} [inst : Ring R] [inst_1 : SetLike S R]
  [toAddGroupConeClass : AddGroupConeClass S R] [toSubmonoidClass : SubmonoidClass S R], RingConeClass S R
-- Lean.Meta.AppBuilder
_private.Lean.Meta.AppBuilder.0.Lean.Meta.infer : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- `Real.exp (f x)` is bounded away from zero along a filter if and only if this filter is bounded
from below under `f`.  -/
Real.isBigO_exp_comp_one : ∀ {α : Type u_1} {l : Filter α} {f : α → ℝ},
  ((fun x => Real.exp (f x)) =O[l] fun x => 1) ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.forIn_eq_forIn_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α × β → δ → m (ForInStep δ)} {init : δ},
  forIn t init f = forIn t.toList init f
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.fst_apply_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] (x : M),
  AddMonoid.Coprod.fst (AddMonoid.Coprod.inl x) = x
-- Mathlib.Algebra.Category.ModuleCat.Products
/-- The concrete product cone is limiting.  -/
ModuleCat.productConeIsLimit : {R : Type u} →
  [inst : Ring R] → {ι : Type v} → (Z : ι → ModuleCat R) → CategoryTheory.Limits.IsLimit (ModuleCat.productCone Z)
-- Mathlib.Data.Fintype.Card
Fintype.card_subtype_le : ∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : Fintype { a // p a }],
  Fintype.card { x // p x } ≤ Fintype.card α
-- Mathlib.Analysis.Real.Spectrum
QuasispectrumRestricts.nnreal_iff : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {a : A},
  QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ quasispectrum ℝ a, 0 ≤ x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.contains_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      (Std.DTreeMap.Raw.Const.insertMany t l).contains k = (t.contains k || (List.map Prod.fst l).contains k)
-- Lean.Parser.Term
Lean.Parser.Term.letIdBinder.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.snd_eq_snd' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (Y Z : CategoryTheory.Over X),
  CategoryTheory.SemiCartesianMonoidalCategory.snd Y Z = CategoryTheory.ChosenPullbacksAlong.snd' Y.hom Z.hom
-- Mathlib.Topology.Maps.Basic
IsOpenMap.mapsTo_interior : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → ∀ {s : Set X} {t : Set Y}, Set.MapsTo f s t → Set.MapsTo f (interior s) (interior t)
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- A submodule over a division ring is an atom of the submodule lattice iff it has `finrank` 1.  -/
Submodule.isAtom_iff_finrank_eq_one : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {S : Submodule K V},
  IsAtom S ↔ Module.finrank K ↥S = 1
-- Mathlib.RingTheory.TensorProduct.Free
Algebra.TensorProduct.basisAux_tmul : ∀ {R : Type u_1} {A : Type u_2} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (b : Module.Basis ι R M) (a : A) (m : M),
  (Algebra.TensorProduct.basisAux A b) (a ⊗ₜ[R] m) = a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.surjective_mk : ∀ {α : Type u_2} {rels : FreeMonoid α → FreeMonoid α → Prop}, Function.Surjective ⇑(PresentedMonoid.mk rels)
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.wPathCasesOn_eta : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {a : P.A} {f : P.last.B a → P.last.W}
  (h : TypeVec.Arrow (P.WPath (WType.mk a f)) α), P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) = h
-- Mathlib.Algebra.Lie.InvariantForm
LieAlgebra.InvariantForm.orthogonal_disjoint : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (Φ : LinearMap.BilinForm R L),
  Φ.Nondegenerate →
    ∀ (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ),
      (∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I) →
        ∀ (I : LieIdeal R L), IsAtom I → Disjoint I (LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv I)
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.Premise.const.sizeOf_spec : ∀ (declName : Lean.Name), sizeOf (Mathlib.Tactic.ClickSuggestions.Premise.const declName) = 1 + sizeOf declName
-- Std.Do.Triple.SpecLemmas
/-- A termination measure for a `repeatM` loop, SVal-typed so it can read monadic state.  -/
Std.Do.WhileVariant : Type u → Std.Do.PostShape → Type u
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
/-- The homotopy relation on `0`-simplices of a simplicial set. It holds
for `x₀` and `x₁` when there exists an edge from `x₀` to `x₁`.  -/
SSet.π₀Rel : {X : SSet} → X.obj (Opposite.op { len := 0 }) → X.obj (Opposite.op { len := 0 }) → Prop
-- Mathlib.Algebra.Homology.Additive
/-- The functor on homological complexes induced by the identity functor is
isomorphic to the identity functor.  -/
CategoryTheory.Functor.mapHomologicalComplexIdIso : {ι : Type u_1} →
  (W₁ : Type u_3) →
    [inst : CategoryTheory.Category.{v_2, u_3} W₁] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms W₁] →
        (c : ComplexShape ι) →
          (CategoryTheory.Functor.id W₁).mapHomologicalComplex c ≅ CategoryTheory.Functor.id (HomologicalComplex W₁ c)
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- Compact-open topology on `C(α, β)` agrees with the topology of uniform convergence on compacts:
a family of continuous functions `F i` tends to `f` in the compact-open topology
if and only if the `F i` tends to `f` uniformly on all compact sets.  -/
ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {ι : Type u₃} {p : Filter ι}
  {F : ι → C(α, β)} {f : C(α, β)},
  Filter.Tendsto F p (nhds f) ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K
-- Mathlib.Analysis.Normed.Group.Uniform
SeparationQuotient.instNormedAddCommGroup.eq_1 : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E],
  SeparationQuotient.instNormedAddCommGroup =
    { toNorm := SeparationQuotient.instNorm, toAddCommGroup := SeparationQuotient.instAddCommGroup,
      toMetricSpace := SeparationQuotient.instMetricSpace, dist_eq := ⋯ }
-- Mathlib.Algebra.Field.Basic
sub_div : ∀ {K : Type u_1} [inst : DivisionRing K] (a b c : K), (a - b) / c = a / c - b / c
-- Init.Core
not_congr : ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
-- Mathlib.GroupTheory.Index
Subgroup.IsFiniteRelIndex.to_finiteIndex_subgroupOf : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [H.IsFiniteRelIndex K], (H.subgroupOf K).FiniteIndex
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
/-- The intervals `(-(n + 1), (n + 1))` form a finite spanning set in the set of open intervals
with rational endpoints for a locally finite measure `μ` on `ℝ`.  -/
Real.finiteSpanningSetsInIooRat : (μ : MeasureTheory.Measure ℝ) →
  [MeasureTheory.IsLocallyFiniteMeasure μ] → μ.FiniteSpanningSetsIn (⋃ a, ⋃ b, ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.d_comp_d_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i j k : ι)
  {Z : V} (h : C.X k ⟶ Z),
  CategoryTheory.CategoryStruct.comp (C.d i j) (CategoryTheory.CategoryStruct.comp (C.d j k) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Extend the total space of a trivialization from the preimage of a set to the whole space.  -/
Bundle.Trivialization.domExtend : {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] →
              {s : Set B} →
                IsOpen (proj ⁻¹' s) →
                  (Bundle.Trivialization F fun z => proj ↑z) → [Nonempty (Z → F)] → Bundle.Trivialization F proj
-- Mathlib.Order.OrderDual
OrderDual.le_toDual : ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ} {b : α}, a ≤ OrderDual.toDual b ↔ b ≤ OrderDual.ofDual a
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.semilatticeSup : {α : Type u_1} → [SemilatticeSup α] → SemilatticeSup (WithZero α)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.toSuccArrow_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (X : C),
  (Φ.toSuccArrow X).right = Φ.succ X
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.singleFunctorsPostcompQIso_inv_hom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (n : ℤ),
  (DerivedCategory.singleFunctorsPostcompQIso C).inv.hom n =
    CategoryTheory.CategoryStruct.id (((CochainComplex.singleFunctors C).postcomp DerivedCategory.Q).functor n)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- The logarithm as an order isomorphism between `Gᵐ⁰ˣ` and `G`.  -/
WithZero.logOrderIso : {G : Type u_3} → [inst : Preorder G] → [inst_1 : AddGroup G] → (WithZero (Multiplicative G))ˣ ≃o G
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddAbove.range_mul : ∀ {ι : Type u_1} {M : Type u_3} [inst : Mul M] [inst_1 : Preorder M] [MulLeftMono M] [MulRightMono M] {f g : ι → M},
  BddAbove (Set.range f) → BddAbove (Set.range g) → BddAbove (Set.range fun i => f i * g i)
-- Std.Net.Addr
/-- Build the IPv6 address `a:b:c:d:e:f:g:h`.
 -/
Std.Net.IPv6Addr.ofParts : UInt16 → UInt16 → UInt16 → UInt16 → UInt16 → UInt16 → UInt16 → UInt16 → Std.Net.IPv6Addr
-- Mathlib.CategoryTheory.DinatTrans
/-- Notation for dinatural transformations.  -/
CategoryTheory.DinatTrans.«term_⤞_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Calculus.Deriv.Inverse
/-- If `f` is an open partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has a
nonzero derivative `f'` at `f.symm a`, then `f.symm` has the derivative `f'⁻¹` at `a`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function.  -/
OpenPartialHomeomorph.hasDerivAt_symm : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (f : OpenPartialHomeomorph 𝕜 𝕜) {a f' : 𝕜},
  a ∈ f.target → f' ≠ 0 → HasDerivAt (↑f) f' (↑f.symm a) → HasDerivAt (↑f.symm) f'⁻¹ a
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.degree_pos_of_irreducible : ∀ {R : Type u} [inst : Field R] {p : Polynomial R}, Irreducible p → 0 < p.degree
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.Iterator.Monadic.step.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α] (it : Std.IterM Id α),
  Std.Rxo.Iterator.Monadic.step it =
    match it.internalState.next with
    | none => Std.IterStep.done
    | some next =>
      if next < it.internalState.upperBound then
        Std.IterStep.yield
          { internalState := { next := Std.PRange.succ? next, upperBound := it.internalState.upperBound } } next
      else Std.IterStep.done
-- Lean.Meta.Basic
/-- Projections `s.i` are reduced at `whnfCore`, and `whnfAtMostI` is used at `s` during the process.
Recall that `whnfAtMostI` is like `whnf` but uses transparency at most `instances`.
This option is stronger than `yes`, but weaker than `yesWithDelta`.
We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations.
When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`,
we only want to unify negation (and not all other field operations as well).
Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986
 -/
Lean.Meta.ProjReductionKind.yesWithDeltaI : Lean.Meta.ProjReductionKind
-- Mathlib.Algebra.Order.Group.Finset
Finset.nsmul_sup' : ∀ {ι : Type u_1} {M : Type u_3} [inst : LinearOrder M] [inst_1 : AddMonoid M] [AddLeftMono M] [AddRightMono M]
  (s : Finset ι) (f : ι → M) (n : ℕ) (hs : s.Nonempty), n • s.sup' hs f = s.sup' hs fun a => n • f a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of a strictly antitone function and an antitone function is
strictly antitone.  -/
StrictAntiOn.add_antitone : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
  [AddLeftMono α] [AddRightStrictMono α], StrictAntiOn f s → AntitoneOn g s → StrictAntiOn (fun x => f x + g x) s
-- Lean.Meta.Tactic.Replace
/-- Replace type of the local declaration with id `fvarId` with one with the same user-facing name, but with type `typeNew`.
This method assumes `eqProof` is a proof that the type of `fvarId` is equal to `typeNew`.
This tactic actually adds a new declaration and (tries to) clear the old one.
If the old one cannot be cleared, then at least its user-facing name becomes inaccessible.

The new local declaration is inserted at the soonest point after `fvarId` at which it is
well-formed. That is, if `typeNew` involves declarations which occur later than `fvarId` in the
local context, the new local declaration will be inserted immediately after the latest-occurring
one. Otherwise, it will be inserted immediately after `fvarId`.
 -/
Lean.MVarId.replaceLocalDecl : Lean.MVarId → Lean.FVarId → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Meta.AssertAfterResult
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.supported_le_supported_iff : ∀ {σ : Type u_1} {R : Type u} [inst : CommSemiring R] {s t : Set σ} [Nontrivial R],
  MvPolynomial.supported R s ≤ MvPolynomial.supported R t ↔ s ⊆ t
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.hsum_embDomain : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (s : HahnSeries.SummableFamily Γ R α) (f : α ↪ β), (s.embDomain f).hsum = s.hsum
-- Mathlib.Analysis.Normed.Group.Bounded
tendsto_norm_atTop_iff_cobounded : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedAddGroup E] {f : α → E} {l : Filter α},
  Filter.Tendsto (fun x => ‖f x‖) l Filter.atTop ↔ Filter.Tendsto f l (Bornology.cobounded E)
-- Init.Data.UInt.Bitwise
instCommutativeUSizeHXor : Std.Commutative fun x1 x2 => x1 ^^^ x2
-- Init.Data.SInt.Bitwise
Int32.and_zero : ∀ {a : Int32}, a &&& 0 = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.ext : ∀ {X : SSet.Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  {x y : SSet.Truncated.Edge x₀ x₁}, x.edge = y.edge → x = y
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Var
Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go_get_aux : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (a curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ)
  (hidx : idx < curr)
  (hfoo : aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w a curr s hcurr).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w a curr s hcurr).vec.get idx ⋯ = (s.get idx hidx).cast hfoo
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.add_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f₁ g₁ f₂ g₂ : u ⟶ v} (h₁ : CategoryTheory.Arrow.LeftHomotopy f₁ g₁)
  (h₂ : CategoryTheory.Arrow.LeftHomotopy f₂ g₂), (h₁.add h₂).hom = h₁.hom + h₂.hom
-- Lean.Language.Basic
/-- Lifts a typed snapshot inside a task to a `SnapshotTree` task by mapping with `f`, propagating the
current transform. Useful in recursive `ToSnapshotTree` instances, where the typeclass instance for
the recursive type is not yet available and `f` is the local recursive function.
 -/
Lean.Language.SnapshotTask.transformWith : {α : Type} →
  Lean.Language.SnapshotTask α →
    (α → Lean.Language.ToSnapshotTreeM Lean.Language.SnapshotTree) →
      Lean.Language.ToSnapshotTreeM (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)
-- Lean.Level
Lean.Level.isExplicit : Lean.Level → Bool
-- Mathlib.Analysis.Analytic.Order
analyticOrderAt_deriv_of_pos : ∀ {𝕜 : Type u_3} {E : Type u_4} [inst : NontriviallyNormedField 𝕜] [CharZero 𝕜] [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] [CompleteSpace E] {f : 𝕜 → E} {z₀ : 𝕜},
  AnalyticAt 𝕜 f z₀ → ∀ {n : ℕ}, analyticOrderAt f z₀ = ↑n + 1 → analyticOrderAt (deriv f) z₀ = ↑n
-- Mathlib.Topology.MetricSpace.Infsep
Set.le_einfsep_pair : ∀ {α : Type u_1} [inst : EDist α] {x y : α}, min (edist x y) (edist y x) ≤ {x, y}.einfsep
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_ofList_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α},
  l.contains k = false → (Std.HashSet.Raw.ofList l).getD k fallback = fallback
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- For a functor `F : C ⥤ D` and an object `d : D`, the category of costructured arrows
`F.obj c ⟶ d` is contravariantly equivalent to the category of structured arrows
`op d ⟶ F.op.obj c`.
 -/
CategoryTheory.costructuredArrowOpEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (d : D) → (CategoryTheory.CostructuredArrow F d)ᵒᵖ ≌ CategoryTheory.StructuredArrow (Opposite.op d) F.op
-- Mathlib.Logic.Equiv.Basic
/-- Note: the "obvious" statement `(piCongrLeft P e) f b = f (e.symm b)` doesn't typecheck: the
LHS would have type `P b` while the RHS would have type `P (e (e.symm b))`. For that reason,
we have to explicitly substitute along `e (e.symm b) = b` in the statement of this lemma.  -/
Equiv.piCongrLeft_apply : ∀ {α : Sort u_1} {β : Sort u_4} (P : β → Sort w) (e : α ≃ β) (f : (a : α) → P (e a)) (b : β),
  (Equiv.piCongrLeft P e) f b = ⋯ ▸ f (e.symm b)
-- Mathlib.Data.Fin.Tuple.Reflection
/-- `FinVec.map f v = ![f (v 0), f (v 1), ...]`  -/
FinVec.map : {α : Type u_1} → {β : Type u_2} → (α → β) → {m : ℕ} → (Fin m → α) → Fin m → β
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.IsBasis.eq_1 : ∀ {α : Type u_2} [inst : TopologicalSpace α] (B : Set (TopologicalSpace.Opens α)),
  TopologicalSpace.Opens.IsBasis B = TopologicalSpace.IsTopologicalBasis (SetLike.coe '' B)
-- Mathlib.Logic.Equiv.Defs
Equiv.symm_trans_apply : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ) (a : γ), (f.trans g).symm a = f.symm (g.symm a)
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.toAlgHom_ofComp_surjective : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_3} {T : Type u_7} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι),
  Function.Surjective ⇑(Q.ofComp P).toAlgHom
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- Every object in `Mat_ C` is isomorphic to the biproduct of its summands.
 -/
CategoryTheory.Mat_.isoBiproductEmbedding : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (M : CategoryTheory.Mat_ C) → M ≅ ⨁ fun i => (CategoryTheory.Mat_.embedding C).obj (M.X i)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_erase_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {k : α}, (m.erase k)[k]! = default
-- Mathlib.Data.Ordmap.Ordset
/-- O(log n). Insert an element into the set, preserving balance and the BST property.
If an equivalent element is already in the set, this replaces it.  -/
Ordset.insert : {α : Type u_1} → [inst : Preorder α] → [Std.Total fun x1 x2 => x1 ≤ x2] → [DecidableLE α] → α → Ordset α → Ordset α
-- Mathlib.Topology.Bases
Topology.IsEmbedding.separableSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [SecondCountableTopology β]
  {f : α → β}, Topology.IsEmbedding f → TopologicalSpace.SeparableSpace α
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.map_frobeniusPoly : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  (MvPolynomial.map (Int.castRingHom ℚ)) (WittVector.frobeniusPoly p n) = WittVector.frobeniusPolyRat p n
-- Mathlib.Data.Multiset.Defs
Multiset.coe_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, ↑l₁ ≤ ↑l₂ ↔ l₁.Subperm l₂
-- Mathlib.Algebra.DirectSum.Internal
/-- Build a `DirectSum.GRing` instance for a collection of additive subgroups.  -/
SetLike.gring : {ι : Type u_1} →
  {σ : Type u_2} →
    {R : Type u_4} →
      [inst : AddMonoid ι] →
        [inst_1 : Ring R] →
          [inst_2 : SetLike σ R] →
            [inst_3 : AddSubgroupClass σ R] → (A : ι → σ) → [SetLike.GradedMonoid A] → DirectSum.GRing fun i => ↥(A i)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullbackIso_hom_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T)
  [inst_1 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)]
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f]
  (i : (CategoryTheory.PreZeroHypercover.pullback₁ f E).I₀),
  (CategoryTheory.PreZeroHypercover.pullbackIso f E).hom.h₀ i = (CategoryTheory.Limits.pullbackSymmetry f (E.f i)).hom
-- Init.Data.String.Basic
String.Slice.endExclusive_sliceTo : ∀ {s : String.Slice} {pos : s.Pos}, (s.sliceTo pos).endExclusive = pos.str
-- Mathlib.Algebra.Module.FinitePresentation
/-- Given a split exact sequence `0 → M → N → P → 0` with `N` finitely presented,
then `M` is also finitely presented.  -/
Module.finitePresentation_of_split_exact : ∀ {R : Type u_2} {M : Type u_4} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : Type u_1} [inst_5 : AddCommGroup P] [inst_6 : Module R P]
  [Module.FinitePresentation R N] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (l : P →ₗ[R] N),
  g ∘ₗ l = LinearMap.id → Function.Injective ⇑f → Function.Exact ⇑f ⇑g → Module.FinitePresentation R M
-- Mathlib.GroupTheory.CommutingProbability
inv_card_commutator_le_commProb : ∀ (G : Type u_2) [inst : Group G] [Finite G], (↑(Nat.card ↥(commutator G)))⁻¹ ≤ commProb G
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.addCommGroupObj : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) →
          (j : J) → AddCommGroup ((F.comp (CategoryTheory.forget (ModuleCat R))).obj j)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_one_le_lift : ∀ {c : Cardinal.{u}}, Cardinal.aleph 1 ≤ Cardinal.lift.{v, u} c ↔ Cardinal.aleph 1 ≤ c