mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDeriv_add : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ ν η : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel ν] [ProbabilityTheory.IsFiniteKernel η]
  (a : α), (κ + ν).rnDeriv η a =ᵐ[η a] κ.rnDeriv η a + ν.rnDeriv η a
-- Lean.Parser.Basic
Lean.Parser.many1NoAntiquot : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.LinearAlgebra.Projection
LinearMap.linearProjOfIsCompl_apply_left : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (q : Submodule R E)
  {F : Type u_7} [inst_3 : AddCommGroup F] [inst_4 : Module R F] (i : F →ₗ[R] E) (hi : Function.Injective ⇑i)
  (h : IsCompl i.range q) (x : F), (LinearMap.linearProjOfIsCompl q i hi h) (i x) = x
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.rightUnitor_neg_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : CategoryTheory.AddGrp C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor G).inv.hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor G.X).inv
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.unop_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F ≅ G),
  CategoryTheory.NatIso.unop α.symm = (CategoryTheory.NatIso.unop α).symm
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.State.mk.inj : ∀ {result? : Option Lean.Meta.AbstractMVarsResult} {generatorStack : Array Lean.Meta.SynthInstance.GeneratorNode}
  {resumeStack : Array (Lean.Meta.SynthInstance.ConsumerNode × Lean.Meta.SynthInstance.Answer)}
  {tableEntries : Std.HashMap Lean.Expr Lean.Meta.SynthInstance.TableEntry}
  {result?_1 : Option Lean.Meta.AbstractMVarsResult} {generatorStack_1 : Array Lean.Meta.SynthInstance.GeneratorNode}
  {resumeStack_1 : Array (Lean.Meta.SynthInstance.ConsumerNode × Lean.Meta.SynthInstance.Answer)}
  {tableEntries_1 : Std.HashMap Lean.Expr Lean.Meta.SynthInstance.TableEntry},
  { result? := result?, generatorStack := generatorStack, resumeStack := resumeStack, tableEntries := tableEntries } =
      { result? := result?_1, generatorStack := generatorStack_1, resumeStack := resumeStack_1,
        tableEntries := tableEntries_1 } →
    result? = result?_1 ∧
      generatorStack = generatorStack_1 ∧ resumeStack = resumeStack_1 ∧ tableEntries = tableEntries_1
-- Init.Data.Array.Attach
Array.findSome?_subtype : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Option β}
  {g : α → Option β}, (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Array.findSome? f xs = Array.findSome? g xs.unattach
-- Mathlib.Data.Sym.Sym2
Sym2.out_snd_mem : ∀ {α : Type u_1} (e : Sym2 α), (Quot.out e).2 ∈ e
-- Mathlib.RingTheory.Perfection
Perfection.instRing : (R : Type u_1) → [inst : CommRing R] → (p : ℕ) → [hp : Fact (Nat.Prime p)] → [CharP R p] → Ring (Perfection R p)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.dmap_eq_some : ∀ {α : Type u} {β : Type v} {o : Option α} {f : (a : α) → o = some a → β} (b : β),
  Std.Internal.List.Option.dmap✝ o f = some b ↔ ∃ a, ∃ (h : o = some a), f a h = b
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = true → t.max? = none
-- Init.Data.String.Iterator
String.Legacy.instInhabitedIterator.default : String.Legacy.Iterator
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_inter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α},
  (m₁ ∩ m₂).getKey! k = if k ∈ m₂ then m₁.getKey! k else default
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.inhabited : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → {N : LieSubmodule R L M} → Inhabited (M ⧸ N)
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
Equiv.divRight₀_apply : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) (x : G₀), (Equiv.divRight₀ a ha) x = x / a
-- Std.Http.Data.Method
Std.Http.Method.proppatch.sizeOf_spec : sizeOf Std.Http.Method.proppatch = 1
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PrepathObject.RightHomotopy.op_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {P : HomotopicalAlgebra.PrepathObject Y}
  {f g : X ⟶ Y} (h : P.RightHomotopy f g), h.op.h = h.h.op
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
/-- Converse to the mean value inequality: if `f` is `C`-lipschitz on a neighborhood of `x₀`
then its line derivative at `x₀` in the direction `v` has norm bounded by `C * ‖v‖`.
Version using `lineDeriv`.  -/
norm_lineDeriv_le_of_lipschitzOn : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {v : E}
  {f : E → F} {x₀ : E} {s : Set E},
  s ∈ nhds x₀ → ∀ {C : NNReal}, LipschitzOnWith C f s → ‖lineDeriv 𝕜 f x₀ v‖ ≤ ↑C * ‖v‖
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.interedges_mono : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {s₁ s₂ t₁ t₂ : Finset α},
  s₂ ⊆ s₁ → t₂ ⊆ t₁ → G.interedges s₂ t₂ ⊆ G.interedges s₁ t₁
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingField.instCommRing : {K : Type v} → [inst : Field K] → (f : Polynomial K) → CommRing f.SplittingField
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.eta`.

---

Eta rule for cocones.  -/
CategoryTheory.Limits.Cocones.eta : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → (c : CategoryTheory.Limits.Cocone F) → c ≅ { pt := c.pt, ι := c.ι }
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Functor.equivCatHom_apply : ∀ (C D : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  (F : CategoryTheory.Functor C D), (CategoryTheory.Functor.equivCatHom C D) F = F.toCatHom
-- Mathlib.Topology.MetricSpace.Closeds
TopologicalSpace.Compacts.lipschitz_sup : ∀ {α : Type u_1} [inst : EMetricSpace α], LipschitzWith 1 fun p => p.1 ⊔ p.2
-- Std.Http.Test.Helpers
/-- Format a single chunk: `<hex-size>\x0d\n<data>\x0d\n`.
 -/
Std.Http.Internal.Test.chunk : String → String
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue?_modifyKey_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValue? k (Std.Internal.List.Const.modifyKey k f l) =
      Option.map f (Std.Internal.List.getValue? k l)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.eval_algebraMap : ∀ {K : Type u} [inst : Field K] {L : Type u} [inst_1 : Field L] (f : K →+* L) (a : L) {S : Type u_1}
  [inst_2 : CommSemiring S] [inst_3 : Algebra S (Polynomial K)] (p : S),
  RatFunc.eval f a ((algebraMap S (RatFunc K)) p) = Polynomial.eval₂ f a ((algebraMap S (Polynomial K)) p)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
/-- Constructor for cochains from a single complex.  -/
CochainComplex.HomComplex.Cochain.fromSingleMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {X : C} →
          {K : CochainComplex C ℤ} →
            {p q : ℤ} →
              (X ⟶ K.X q) →
                {n : ℤ} → p + n = q → CochainComplex.HomComplex.Cochain ((CochainComplex.singleFunctor C p).obj X) K n
-- Init.Notation
/-- `#check_tactic_failure t by tac` runs the tactic `tac`
on a goal with `t` and verifies it fails.
 -/
Lean.Parser.checkTacticFailure : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableOn_add_const_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} (c : F), DifferentiableOn 𝕜 (fun y => f y + c) s ↔ DifferentiableOn 𝕜 f s
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.natCast_mem_one : ∀ {R : Type u_2} [inst : AddMonoidWithOne R] (n : ℕ), ↑n ∈ 1
-- Init.Data.Vector.Lemmas
Vector.setIfInBounds_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n) {i : ℕ} {x : α},
  (Vector.mk xs h).setIfInBounds i x = Vector.mk (xs.setIfInBounds i x) ⋯
-- Init.Data.Slice.Array.Lemmas
Array.array_mkSlice_rcc : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ}, (Std.Rcc.Sliceable.mkSlice xs lo...=hi).array = xs
-- Init.Data.Iterators.Basic
/-- A relation that governs the allowed steps from a given iterator.

The "plausible" steps are those which make sense for a given state; plausibility can ensure
properties such as the successor iterator being drawn from the same collection, that an iterator
resulting from a skip will return the same next value, or that the next item yielded is next one
in the original collection.
 -/
Std.Iterator.IsPlausibleStep : {α : Type w} →
  {m : Type w → Type w'} →
    {β : outParam (Type w)} → [self : Std.Iterator α m β] → Std.IterM m β → Std.IterStep (Std.IterM m β) β → Prop
-- Mathlib.RingTheory.Ideal.Operations
Ideal.sum_eq_sup : ∀ {R : Type u} [inst : Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Ideal R), s.sum f = s.sup f
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.Path.le : ∀ {J : Type u_1} [inst : LinearOrder J] {i j : J} (f : CategoryTheory.SimplicialThickening.Path i j), i ≤ j
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The functor sending a topological representation to the corresponding object in
`Action (TopModuleCat k) G`.  -/
TopRep.toActionTopModFunc : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] →
      [inst_1 : Ring k] → [inst_2 : Monoid G] → CategoryTheory.Functor (TopRep k G) (Action (TopModuleCat k) G)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.toArray_succ_succ_eq_map : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α] [DecidableLT α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_8 : Std.PRange.InfinitelyUpwardEnumerable α] [inst_9 : Std.Rxc.IsAlwaysFinite α]
  [inst_10 : Std.PRange.LawfulUpwardEnumerable α] {lo hi : α},
  ((Std.PRange.succ lo)<...=Std.PRange.succ hi).toArray = Array.map Std.PRange.succ (lo<...=hi).toArray
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.size : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → ℕ
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.Break.runK.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.condIndepFun_prodMk : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {β : ι → Type u_6}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.CondIndepFun m' hm' (fun a => (f i a, f j a)) (f k) μ
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulDysonETransform.card : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.mulDysonETransform e x).1.card + (Finset.mulDysonETransform e x).2.card = x.1.card + x.2.card
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.IsRegularEpi.desc.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f f_1 : X ⟶ Y) (e_f : f = f_1)
  [inst_1 : CategoryTheory.IsRegularEpi f] (k k_1 : X ⟶ Z) (e_k : k = k_1)
  (h :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularEpi.left f) k =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularEpi.right f) k),
  CategoryTheory.IsRegularEpi.desc f k h = CategoryTheory.IsRegularEpi.desc f_1 k_1 ⋯
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Over.isoMk_inv_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : Q.RespectsIso] {A B : P.Over Q X} (f : A.left ≅ B.left)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp f.hom B.hom = A.hom)
      CategoryTheory.MorphismProperty.Over.isoMk._auto_1),
  (CategoryTheory.MorphismProperty.Over.isoMk f w).inv.left = f.inv
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsMatch.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {endPos : s.Pos},
  String.Slice.Pattern.Model.PatternModel.Matches pat (s.sliceTo endPos).copy →
    String.Slice.Pattern.Model.IsMatch pat endPos
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivAt.clm_comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {x : 𝕜}
  {G : Type u_2} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {c : 𝕜 → F →L[𝕜] G} {c' : F →L[𝕜] G}
  {d : 𝕜 → E →L[𝕜] F} {d' : E →L[𝕜] F},
  HasDerivAt c c' x → HasDerivAt d d' x → HasDerivAt (fun y => c y ∘SL d y) (c' ∘SL d x + c x ∘SL d') x
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.collectFVars : Lean.Meta.Match.Pattern → StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit
-- Lean.Widget.Types
Lean.Widget.Module.mk.inj : ∀ {javascript : String} {javascriptHash : { x // x = hash javascript }} {javascript_1 : String}
  {javascriptHash_1 : { x // x = hash javascript_1 }},
  { javascript := javascript, javascriptHash := javascriptHash } =
      { javascript := javascript_1, javascriptHash := javascriptHash_1 } →
    javascript = javascript_1 ∧ javascriptHash ≍ javascriptHash_1
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.logEquiv_apply : ∀ {G : Type u_5} [inst : AddGroup G] (x : (WithZero (Multiplicative G))ˣ), WithZero.logEquiv x = (↑x).log
-- Mathlib.Tactic.Push.Attr
/-- Checks if the expression has the head in any subexpression.
We don't need to check this for `.lambda`, because the term being a function
is sufficient for `pull fun _ ↦ _` to be applicable.  -/
_private.Mathlib.Tactic.Push.Attr.0.Mathlib.Tactic.Push.isPullThm.containsHead : Lean.Expr → Mathlib.Tactic.Push.Head → Bool
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.overEquiv_symm_pullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y₁ Y₂ : CategoryTheory.Over X} (f : Y₁ ⟶ Y₂)
  (S : CategoryTheory.Sieve Y₂.left),
  (CategoryTheory.Sieve.overEquiv Y₁).symm (CategoryTheory.Sieve.pullback (CategoryTheory.Over.Hom.left f) S) =
    CategoryTheory.Sieve.pullback f ((CategoryTheory.Sieve.overEquiv Y₂).symm S)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_maxKey?_of_isSome_maxKey?_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.erase k).maxKey?.isSome = true → t.maxKey?.isSome = true
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instInhabitedExpr.default : Lean.Grind.CommRing.Expr
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
/-- The good products span all of `LocallyConstant C ℤ` if `C` is closed.  -/
Profinite.NobelingProof.GoodProducts.span : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [WellFoundedLT I],
  IsClosed C → ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval C))
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.empty : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → aig.RefVec 0
-- Mathlib.Topology.UniformSpace.Cauchy
CauchySeq.subseq_subseq_mem : ∀ {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → SetRel α α},
  (∀ (n : ℕ), V n ∈ uniformity α) →
    ∀ {u : ℕ → α},
      CauchySeq u →
        ∀ {f g : ℕ → ℕ},
          Filter.Tendsto f Filter.atTop Filter.atTop →
            Filter.Tendsto g Filter.atTop Filter.atTop →
              ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of a meromorphic function `f` at `z₀`, as an element of `ℤ ∪ {∞}`.

The order is defined to be `∞` if `f` is identically 0 on a neighbourhood of `z₀`, and otherwise the
unique `n` such that `f` can locally be written as `f z = (z - z₀) ^ n • g z`, where `g` is analytic
and does not vanish at `z₀`. See `MeromorphicAt.meromorphicOrderAt_eq_top_iff` and
`MeromorphicAt.meromorphicOrderAt_eq_int_iff` for these equivalences.

If the function is not meromorphic at `x`, we use the junk value `0`.  -/
meromorphicOrderAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → 𝕜 → WithTop ℤ
-- Init.Data.UInt.Lemmas
UInt64.le_rfl : ∀ {a : UInt64}, a ≤ a
-- Mathlib.LinearAlgebra.Matrix.Vec
/-- The Hadamard bilinear form equals the Kronecker bilinear form on diagonal embeddings.  -/
Matrix.dotProduct_hadamard_mulVec_eq_kronecker : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : NonUnitalSemiring R] [inst_1 : DecidableEq m]
  [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n] (x : m → R) (A B : Matrix m n R) (x' : n → R),
  x ⬝ᵥ (A.hadamard B).mulVec x' =
    (Matrix.diagonal x).vec ⬝ᵥ (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B).mulVec (Matrix.diagonal x').vec
-- Mathlib.Data.Sign.Basic
SignType.coe_zpow : ∀ {α : Type u_1} [inst : GroupWithZero α] [inst_1 : HasDistribNeg α] (a : SignType) (k : ℤ), ↑(a ^ k) = ↑a ^ k
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- The supremum of `insert a s` is the maximum of `a` and the supremum of `s`, if `s` is
nonempty and bounded above.  -/
csSup_insert : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α},
  BddAbove s → s.Nonempty → sSup (insert a s) = a ⊔ sSup s
-- Init.Prelude
_private.Init.Prelude.0.Lean.extractMacroScopesAux : Lean.Name → List Lean.MacroScope → Lean.MacroScopesView
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.prop : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  (self : CategoryTheory.MorphismProperty.Comma L R P Q W), P self.hom
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.continuous_valuation_of_surjective : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [hv : Valued K Γ₀], Function.Surjective ⇑Valued.v → Continuous ⇑Valued.v
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.modifyTR.go.eq_1 : ∀ {α : Type u_1} (f : α → α) (a : ℕ) (a_1 : Array α), List.modifyTR.go✝ f [] a a_1 = a_1.toList
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.image_coe_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithTop.some '' Set.Ici a = Set.Ico ↑a ⊤
-- Mathlib.Order.Hom.Lattice
instCoeTCSupHomOfSupHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] → [inst_1 : Max α] → [inst_2 : Max β] → [SupHomClass F α β] → CoeTC F (SupHom α β)
-- Mathlib.Data.WSeq.Defs
/-- Returns `true` if every element of `s` satisfies `p`  -/
Stream'.WSeq.all : {α : Type u} → Stream'.WSeq α → (α → Bool) → Computation Bool
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (n m : ℤ)
  (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app._auto_1),
  (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app
        (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X))))
      ((CategoryTheory.shiftFunctorCompIsoId C n m hnm).inv.app (Opposite.unop X)).op
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_minKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false → Std.Internal.List.containsKey (Std.Internal.List.minKey! l) l = true
-- Init.Data.Array.Lemmas
Array.or_all_distrib_left : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool} {q : Bool}, (q || xs.all p) = xs.all fun a => q || p a
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.IsExtension.extension_L : ∀ {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : LieRing N] [inst_4 : LieAlgebra R N] [inst_5 : LieRing M]
  [inst_6 : LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : LieAlgebra.IsExtension i p), h.extension.L = L
-- Mathlib.RingTheory.Finiteness.FiniteTypeLocal
Algebra.FiniteType.of_span_eq_top_source : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R),
  Ideal.span s = ⊤ →
    (∀ i ∈ s, Algebra.FiniteType (Localization.Away i) (TensorProduct R (Localization.Away i) S)) →
      Algebra.FiniteType R S
-- Mathlib.GroupTheory.Nilpotent
_private.Mathlib.GroupTheory.Nilpotent.0.Subgroup.upperCentralSeriesAux.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- A block matrix is invertible if the top left corner and the corresponding Schur complement
is.  -/
Matrix.fromBlocks₁₁Invertible : {m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_4} →
      [inst : Fintype m] →
        [inst_1 : Fintype n] →
          [inst_2 : DecidableEq m] →
            [inst_3 : DecidableEq n] →
              [inst_4 : CommRing α] →
                (A : Matrix m m α) →
                  (B : Matrix m n α) →
                    (C : Matrix n m α) →
                      (D : Matrix n n α) →
                        [inst_5 : Invertible A] → [Invertible (D - C * ⅟A * B)] → Invertible (Matrix.fromBlocks A B C D)
-- Mathlib.LinearAlgebra.FreeModule.PID
Module.Basis.SmithNormalForm.repr_comp_embedding_eq_smul : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {n : ℕ} {N : Submodule R M} (snf : Module.Basis.SmithNormalForm N ι n) (m : ↥N),
  ⇑(snf.bM.repr ↑m) ∘ ⇑snf.f = snf.a • ⇑(snf.bN.repr m)
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- The tilde-Gamma adjunction.  -/
AlgebraicGeometry.tilde.adjunction : {R : CommRingCat} → AlgebraicGeometry.tilde.functor R ⊣ AlgebraicGeometry.moduleSpecΓFunctor