mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry?.induct_unfolding : ∀ {α : Type u} {β : α → Type v} (motive : Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a) → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf none →
    (∀ (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) (some ⟨k, v⟩)) →
      (∀ (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
          (l_1 r : Std.DTreeMap.Internal.Impl α β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)
              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxEntry? →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxEntry?) →
        ∀ (a : Std.DTreeMap.Internal.Impl α β), motive a a.maxEntry?
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_add_nonpos_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a b : α}, -a + b ≤ 0 ↔ b ≤ a
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.replaceHead.congr_simp : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j : ι} (x x_1 : M i) (e_x : x = x_1)
  (_hnotone : x ≠ 1) (_w _w_1 : Monoid.CoprodI.NeWord M i j),
  _w = _w_1 → Monoid.CoprodI.NeWord.replaceHead x _hnotone _w = Monoid.CoprodI.NeWord.replaceHead x_1 ⋯ _w_1
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- If `F ⋙ G` preserves colimits of shape `J` and `G` reflects colimits of shape `J`, then `F`
preserves colimits of shape `J`.
 -/
CategoryTheory.Limits.preservesColimitsOfShape_of_reflects_of_preserves : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  [CategoryTheory.Limits.PreservesColimitsOfShape J (F.comp G)] [CategoryTheory.Limits.ReflectsColimitsOfShape J G],
  CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `link2` which can be used in the absence of balance information but
still assumes the preconditions of `link2`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.link2! : {α : Type u} →
  {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Topology.Order.LeftRightLim
Antitone.le_rightLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Antitone f → ∀ {x y : α}, x < y → f y ≤ Function.rightLim f x
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Scheme.Etale.forget_obj_left : ∀ (X : AlgebraicGeometry.Scheme) (Y : X.Etale), ((AlgebraicGeometry.Scheme.Etale.forget X).obj Y).left = Y.left
-- Mathlib.Tactic.NormNum.Result
/-- Helper function to synthesize a typed `AddMonoidWithOne α` expression.  -/
Mathlib.Meta.NormNum.inferAddMonoidWithOne : {u : Lean.Level} → (α : Q(Type u)) → Lean.MetaM Q(AddMonoidWithOne «$α»)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ColorInformation.range : Lean.Lsp.ColorInformation → Lean.Lsp.Range
-- Std.Net.Addr
Std.Net.SocketAddressV4.mk.sizeOf_spec : ∀ (addr : Std.Net.IPv4Addr) (port : UInt16), sizeOf { addr := addr, port := port } = 1 + sizeOf addr + sizeOf port
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.toSubsemiring : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : AddMonoid ι] →
        [inst_1 : Semiring A] →
          [inst_2 : SetLike σ A] →
            [inst_3 : AddSubmonoidClass σ A] →
              {𝒜 : ι → σ} →
                [inst_4 : DecidableEq ι] → [inst_5 : GradedRing 𝒜] → HomogeneousSubsemiring 𝒜 → Subsemiring A
-- Mathlib.Logic.Equiv.Defs
Equiv.coe_inj : ∀ {α : Sort u} {β : Sort v} {e₁ e₂ : α ≃ β}, ⇑e₁ = ⇑e₂ ↔ e₁ = e₂
-- Mathlib.Topology.Algebra.AffineSubspace
AffineSubspace.subtypeA_toAffineMap : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (s : AffineSubspace R P) [inst_5 : Nonempty ↥s],
  ↑s.subtypeA = s.subtype
-- Plausible.Random
/-- Given a random generator for `α`, we can convert it to a random generator for `ULift α`.  -/
Plausible.RandT.up : {α : Type u} →
  {m : Type u → Type w} →
    {m' : Type (max u v) → Type w'} →
      {g : Type} →
        [RandomGen g] →
          [Monad m] →
            [Monad m'] →
              ({α : Type u} → m α → m' (ULift.{v, u} α)) →
                Plausible.RandGT g m α → Plausible.RandGT g m' (ULift.{v, u} α)
-- Mathlib.Tactic.Simps.NotationClass
/-- Find arguments for the `Zero` class.  -/
Simps.findZeroArgs : Simps.findArgType
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.Corec.f.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (val : β) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (val : β) → motive (Sum.inr val)),
  (match Sum.inr val with
    | Sum.inl a => h_1 a
    | Sum.inr val => h_2 val) =
    h_2 val
-- Std.Data.ByteSlice
_private.Std.Data.ByteSlice.0.ByteSlice.forM.loop.eq_def : ∀ {m : Type v → Type w} [inst : Monad m] (f : UInt8 → m PUnit.{v + 1}) (as : ByteSlice) (i : ℕ),
  ByteSlice.forM.loop✝ f as i =
    if h : i < as.size then do
      f as[i]
      ByteSlice.forM.loop✝ f as (i + 1)
    else pure PUnit.unit
-- Init.Data.String.Lemmas.Order
String.Pos.le_ofSliceFrom_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos},
  q ≤ String.Pos.ofSliceFrom p ↔ ∀ (h : p₀ ≤ q), p₀.sliceFrom q h ≤ p
-- Mathlib.Order.RelClasses
instIsPreorderLe : ∀ {α : Type u} [inst : Preorder α], IsPreorder α fun x1 x2 => x1 ≤ x2
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.IsPathGraph3Compl.fst_ne_snd : ∀ {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α}, G.IsPathGraph3Compl v w₁ w₂ → w₁ ≠ w₂
-- Init.Data.BitVec.Bitblast
BitVec.toInt_sdiv : ∀ {w : ℕ} (a b : BitVec w), (a.sdiv b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ w)
-- Mathlib.Data.Multiset.Filter
Multiset.filterMap_eq_map : ∀ {α : Type u_1} {β : Type v} (f : α → β), Multiset.filterMap (some ∘ f) = Multiset.map f
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.isStackFor_ofArrows_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} (f : (i : ι) → X i ⟶ S),
  F.IsStackFor (CategoryTheory.Presieve.ofArrows X f) ↔ (F.toDescentData f).IsEquivalence
-- Init.Data.BitVec.Lemmas
BitVec.le_def : ∀ {n : ℕ} {x y : BitVec n}, x ≤ y ↔ x.toNat ≤ y.toNat
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.waitForExit : Lean.Lsp.Ipc.IpcM UInt32
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.empty_equiv_iff_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp}, Std.TreeSet.empty.Equiv t ↔ t.isEmpty = true
-- Mathlib.RingTheory.PolynomialAlgebra
PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_1 : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (p : Polynomial R)
  (k : ℕ) (h : Decidable ¬p.coeff k = 0) (a : A),
  (if ¬p.coeff k = 0 then a * (algebraMap R A) (p.coeff k) else 0) = a * (algebraMap R A) (p.coeff k)
-- Mathlib.GroupTheory.CoprodI
/-- The remaining letters of the word, excluding the first letter  -/
Monoid.CoprodI.Word.Pair.tail : {ι : Type u_1} →
  {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → {i : ι} → Monoid.CoprodI.Word.Pair M i → Monoid.CoprodI.Word M
-- Mathlib.MeasureTheory.Integral.TorusIntegral
torusMap.eq_1 : ∀ {n : ℕ} (c : Fin n → ℂ) (R θ : Fin n → ℝ) (i : Fin n),
  torusMap c R θ i = c i + ↑(R i) * Complex.exp (↑(θ i) * Complex.I)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (X : C) {Z : C}
  (h : (t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X)))
      (CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X) h) =
    CategoryTheory.CategoryStruct.comp ((t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X))) h
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- Let `A` be an algebraically closed field and let `x ∈ K`, with `K/F` an algebraic extension
of fields. Then the images of `x` by the `F`-algebra morphisms from `K` to `A` are exactly
the roots in `A` of the minimal polynomial of `x` over `F`.  -/
Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly : ∀ {F : Type u_1} {K : Type u_2} (A : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field A]
  [inst_3 : Algebra F K] [inst_4 : Algebra F A] [Algebra.IsAlgebraic F K] [IsAlgClosed A] (x : K),
  (Set.range fun ψ => ψ x) = (minpoly F x).rootSet A
-- Mathlib.Algebra.MvPolynomial.Basic
/-- `MvPolynomial.coeff m` but promoted to a `LinearMap`.  -/
MvPolynomial.lcoeff : (R : Type u) → {σ : Type u_1} → [inst : CommSemiring R] → (σ →₀ ℕ) → MvPolynomial σ R →ₗ[R] R
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- Constructor for null homotopic morphisms, see also `Homotopy.ofNullHomotopic`
and `Homotopy.eq_add_nullHomotopic`.  -/
CategoryTheory.ShortComplex.nullHomotopic : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (S₁ S₂ : CategoryTheory.ShortComplex C) →
        (h₀ : S₁.X₁ ⟶ S₂.X₁) →
          CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0 →
            (S₁.X₂ ⟶ S₂.X₁) →
              (S₁.X₃ ⟶ S₂.X₂) → (h₃ : S₁.X₃ ⟶ S₂.X₃) → CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0 → (S₁ ⟶ S₂)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The direction of an affine subspace constructed from a point and a direction.  -/
AffineSubspace.direction_mk' : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p : P) (direction : Submodule k V), (AffineSubspace.mk' p direction).direction = direction
-- Lean.Util.SCC
_private.Lean.Util.SCC.0.Lean.SCC.updateLowLinkOf : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → α → Option ℕ → Lean.SCC.M α Unit
-- Init.Data.Nat.Coprime
Nat.Coprime.symm : ∀ {n m : ℕ}, n.Coprime m → m.Coprime n
-- Init.Data.Nat.Basic
Nat.add_one_ne_zero : ∀ (n : ℕ), n + 1 ≠ 0
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.mk.injEq : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  (toStarSubalgebra : StarSubalgebra ℂ (H →L[ℂ] H))
  (centralizer_centralizer' : toStarSubalgebra.carrier.centralizer.centralizer = toStarSubalgebra.carrier)
  (toStarSubalgebra_1 : StarSubalgebra ℂ (H →L[ℂ] H))
  (centralizer_centralizer'_1 : toStarSubalgebra_1.carrier.centralizer.centralizer = toStarSubalgebra_1.carrier),
  ({ toStarSubalgebra := toStarSubalgebra, centralizer_centralizer' := centralizer_centralizer' } =
      { toStarSubalgebra := toStarSubalgebra_1, centralizer_centralizer' := centralizer_centralizer'_1 }) =
    (toStarSubalgebra = toStarSubalgebra_1)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_iInf_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {ι : Type u_5} {f : M →ₙ+ N},
  Function.Surjective ⇑f →
    ∀ (S : ι → AddSubsemigroup N), AddSubsemigroup.map f (⨅ i, AddSubsemigroup.comap f (S i)) = iInf S
-- Mathlib.Data.Finset.Powerset
/-- **Alias** of the reverse direction of `Finset.powersetCard_nonempty`. -/
Finset.powersetCard_nonempty_of_le : ∀ {α : Type u_1} {n : ℕ} {s : Finset α}, n ≤ s.card → (Finset.powersetCard n s).Nonempty
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Ideal.IsMinimalPrime.le : ∀ {R : Type u_1} [inst : CommSemiring R] {I p : Ideal R}, I.IsMinimalPrime p → I ≤ p
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_univ_right : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommGroup α] [inst_2 : Fintype α] (s : Finset α),
  s.mulEnergy Finset.univ = Fintype.card α * s.card ^ 2
-- Mathlib.NumberTheory.Divisors
/-- Useful lemma for reordering sums.  -/
Nat.divisorsAntidiagonal_eq_prod_filter_of_le : ∀ {n N : ℕ}, n ≠ 0 → n ≤ N → n.divisorsAntidiagonal = {x ∈ Finset.Ioc 0 N ×ˢ Finset.Ioc 0 N | x.1 * x.2 = n}
-- Mathlib.Analysis.Calculus.Rademacher
/-- If a Lipschitz functions has line derivatives in a dense set of directions, all of them given by
a single continuous linear map `L`, then it admits `L` as Fréchet derivative.  -/
LipschitzWith.hasFDerivAt_of_hasLineDerivAt_of_closure : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {C : NNReal} [FiniteDimensional ℝ E] {f : E → F},
  LipschitzWith C f →
    ∀ {s : Set E},
      Metric.sphere 0 1 ⊆ closure s →
        ∀ {L : E →L[ℝ] F} {x : E}, (∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v) → HasFDerivAt f L x
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.toQ_inj : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] [Lean.Grind.AddRightCancel α] {a b : α}, ↑a = ↑b → a = b
-- Mathlib.Algebra.Group.Units.Hom
IsAddUnit.of_leftInverse : ∀ {F : Type u_1} {G : Type u_2} {M : Type u_3} {N : Type u_4} [inst : FunLike F M N] [inst_1 : FunLike G N M]
  [inst_2 : AddMonoid M] [inst_3 : AddMonoid N] [AddMonoidHomClass G N M] {f : F} {x : M} (g : G),
  Function.LeftInverse ⇑g ⇑f → IsAddUnit (f x) → IsAddUnit x
-- Mathlib.Analysis.Quaternion
Quaternion.instNormOneClassReal : NormOneClass (Quaternion ℝ)
-- Mathlib.Order.Filter.Pointwise
Filter.instNSMul.eq_1 : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : Add α], Filter.instNSMul = { smul := fun n s => nsmulRec n s }
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryGTD : {α : Type u} → {β : Type v} → [Ord α] → α → (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → α × β
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.EvalConfigItemHandler.mk : Lean.Syntax →
  Lean.Name →
    Lean.Elab.ConfigEval.EvalConfigItemHandlerKind →
      Lean.Term → Option Lean.Name → Option Lean.Name → Lean.Elab.ConfigEval.EvalConfigItemHandler
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.incidence_other_prop : ∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] {v : V} {e : Sym2 V} (h : e ∈ G.incidenceSet v),
  G.otherVertexOfIncident h ∈ G.neighborSet v
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.one_def : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [inst : Semiring A] [inst_1 : SetLike σ A] {𝒜 : ι → σ},
  1 = GradedRingHom.id 𝒜
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.WeaklyEtale.instMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.WeaklyEtale f],
  AlgebraicGeometry.WeaklyEtale (f ∣_ V)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.instIsSplitEpiFst : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q), CategoryTheory.IsSplitEpi c.fst
-- Mathlib.Algebra.MvPolynomial.Funext
MvPolynomial.funext_set_iff : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {σ : Type u_2} {p q : MvPolynomial σ R} (s : σ → Set R),
  (∀ (i : σ), (s i).Infinite) → (p = q ↔ ∀ x ∈ Set.univ.pi s, (MvPolynomial.eval x) p = (MvPolynomial.eval x) q)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_le_iff_colorable : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ}, G.chromaticNumber ≤ ↑n ↔ G.Colorable n
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop.eq_1 : ∀ {M : Type u_2} [inst : MulOneClass M] (x : Submonoid Mᵐᵒᵖ),
  x.unop = { carrier := MulOpposite.op ⁻¹' ↑x, mul_mem' := ⋯, one_mem' := ⋯ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.of_forall_getKey?_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.DTreeMap α (fun x => Unit) cmp},
  (∀ (k : α), t₁.getKey? k = t₂.getKey? k) → t₁.Equiv t₂
-- Mathlib.Analysis.Meromorphic.IsolatedZeros
/-- Variant of the principle of isolated zeros: Let `U` be a subset of `𝕜` and assume that `x ∈ U` is
not an isolated point of `U`. If a function `f` is meromorphic at `x` and vanishes along a subset
that is codiscrete within `U`, then `f` vanishes in a punctured neighbourhood of `f`.

For a typical application, let `U` be a path in the complex plane and let `x` be one of the end
points. If `f` is meromorphic at `x` and vanishes on `U`, then it will vanish in a punctured
neighbourhood of `x`, which intersects `U` non-trivially but is not contained in `U`.

The assumption that `x` is not an isolated point of `U` is expressed as `AccPt x (𝓟 U)`. See
`accPt_iff_frequently` and `accPt_iff_frequently_nhdsNE` for useful reformulations.
 -/
MeromorphicAt.eventuallyEq_zero_nhdsNE_of_eventuallyEq_zero_codiscreteWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {x : 𝕜} {f : 𝕜 → E},
  MeromorphicAt f x →
    x ∈ U → AccPt x (Filter.principal U) → f =ᶠ[Filter.codiscreteWithin U] 0 → f =ᶠ[nhdsWithin x {x}ᶜ] 0
-- Mathlib.Topology.Compactness.Compact
/-- The coproduct of the cocompact filters on two topological spaces is the cocompact filter on
their product.  -/
Filter.coprod_cocompact : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  (Filter.cocompact X).coprod (Filter.cocompact Y) = Filter.cocompact (X × Y)
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- We define `mFourierBasis` to be a `ℤᵈ`-indexed Hilbert basis for the `L²` space of functions
on `UnitAddTorus d`, which by definition is an isometric isomorphism from `L²(UnitAddTorus d)`
to `ℓ²(ℤᵈ, ℂ)`.  -/
UnitAddTorus.mFourierBasis : {d : Type u_1} → [inst : Fintype d] → HilbertBasis (d → ℤ) ℂ ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)
-- Init.Data.SInt.Bitwise
Int8.and_self : ∀ {a : Int8}, a &&& a = a
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
CategoryTheory.ObjectProperty.localEpi_top_eq_epimorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  ⊤.localEpi = CategoryTheory.MorphismProperty.epimorphisms C
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesMap_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S₁ S₂ : CategoryTheory.ShortComplex C) [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology],
  CategoryTheory.ShortComplex.opcyclesMap 0 = 0
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] {g₁ g₂ : CompleteLatticeHom β γ} {f : CompleteLatticeHom α β},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_sInter_eq_biInter_closure_of_sUnion_indep : ∀ {α : Type u_2} {M : Matroid α} (Is : Set (Set α)),
  Is.Nonempty → M.Indep (⋃₀ Is) → M.closure (⋂₀ Is) = ⋂ I ∈ Is, M.closure I
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₀₁_le_rpow_sub_two_mul_self : ∀ {p t x : ℝ}, p ∈ Set.Ioo 0 1 → 0 < t → 0 ≤ x → p.rpowIntegrand₀₁ t x ≤ t ^ (p - 2) * x
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyLE? : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → Option α
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.mk : {R : Type u_1} →
  [inst : CommRing R] →
    (f : Polynomial R) →
      f.Monic → (g : Polynomial R) → (∃ p₁ p₂ n, Polynomial.derivative f * p₁ + f * p₂ = g ^ n) → StandardEtalePair R
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.convs'.eq_1 : ∀ {K : Type u_2} [inst : DivisionRing K] (g : GenContFract K) (n : ℕ), g.convs' n = g.h + GenContFract.convs'Aux g.s n
-- Mathlib.Topology.Instances.CantorSet
cantorSequence.eq_1 : ∀ (x : ℝ), cantorSequence x = Stream'.iterate cantorStep x
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.image_closedBall : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (x : α) (r : ℝ),
  ⇑h '' Metric.closedBall x r = Metric.closedBall (h x) r
-- Mathlib.Order.Defs.Unbundled
/-- A lower set in an order `α` is a set such that any element less than one of its
members is also a member. Also called down-set, downward-closed set.  -/
IsLowerSet : {α : Type u_1} → [LE α] → Set α → Prop
-- Mathlib.FieldTheory.Galois.Basic
IsAlgClosure.isGalois : ∀ (k : Type u_1) (K : Type u_2) [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [IsAlgClosure k K]
  [CharZero k], IsGalois k K
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Min α] →
      [inst_1 : Min β] →
        [inst_2 : Top α] → [inst_3 : Top β] → (toInfHom : InfHom α β) → toInfHom.toFun ⊤ = ⊤ → InfTopHom α β
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.Slice.intercalate.go.eq_def : ∀ (acc : String) (s : String.Slice) (a : List String.Slice),
  String.Slice.intercalate.go✝ acc s a =
    match a with
    | a :: as => String.Slice.intercalate.go✝ (acc ++ s ++ a) s as
    | [] => acc
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.add_iff : ∀ {M : Type u_1} [inst : AddMonoid M] [IsDedekindFiniteAddMonoid M] {x y : M},
  IsAddUnit (x + y) ↔ IsAddUnit x ∧ IsAddUnit y
-- Aesop.Index.RulePattern
/-- Get all substitutions of the rule patterns that match a subexpression of
`e`. Subexpressions containing bound variables are not considered. The returned
array may contain duplicates.  -/
Aesop.RulePatternIndex.get : Lean.Expr → Aesop.RulePatternIndex → Aesop.BaseM Aesop.RulePatternSubstMap
-- Init.Data.List.Basic
/-- A member of the tail of a list is a member of the list: `a ∈ l → a ∈ b :: l`.  -/
List.Mem.tail : ∀ {α : Type u} {a : α} (b : α) {as : List α}, List.Mem a as → List.Mem a (b :: as)
-- Mathlib.Algebra.Module.ZMod
ZMod.smul_mem : ∀ {n : ℕ} {M : Type u_1} {S : Type u_4} [inst : AddCommGroup M] [inst_1 : Module (ZMod n) M] [inst_2 : SetLike S M]
  [AddSubgroupClass S M] {x : M} {K : S}, x ∈ K → ∀ (c : ZMod n), c • x ∈ K
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.skeleton_skeletal : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], CategoryTheory.Skeletal (CategoryTheory.Skeleton C)