mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
/-- A local ring homomorphism into a field can be descended onto the residue field.  -/
IsLocalRing.ResidueField.lift : {R : Type u_4} →
  {S : Type u_5} →
    [inst : CommRing R] →
      [inst_1 : IsLocalRing R] → [inst_2 : Field S] → (f : R →+* S) → [IsLocalHom f] → IsLocalRing.ResidueField R →+* S
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableAt.mvfderiv : ∀ {𝕜 : 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'] {x : M} {f : M → E'},
  MDiffAt f x →
    d% f x = fderivWithin 𝕜 (writtenInExtChartAt I (modelWithCornersSelf 𝕜 E') x f) (Set.range ↑I) (↑(extChartAt I x) x)
-- Mathlib.SetTheory.ZFC.Rank
/-- `ZFSet.rank` is equal to the `IsWellFounded.rank` over `∈`.  -/
ZFSet.rank_eq_wfRank : ∀ {x : ZFSet.{u}}, Ordinal.lift.{u + 1, u} x.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) x
-- Std.Time.Date.Unit.Month
/-- The ordinal value representing the month of March.
 -/
Std.Time.Month.Ordinal.march : Std.Time.Month.Ordinal
-- Mathlib.Order.Filter.NAry
Filter.mem_map₂_iff : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β} {u : Set γ},
  u ∈ Filter.map₂ m f g ↔ ∃ s ∈ f, ∃ t ∈ g, Set.image2 m s t ⊆ u
-- Mathlib.Order.WellFoundedSet
Set.wellFoundedOn_singleton : ∀ {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {a : α}, {a}.WellFoundedOn r
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.unzeroD_mono : ∀ {α : Type u_1} [inst : LE α] {x y : WithZero α} {a : α}, x ≠ 0 → x ≤ y → WithZero.unzeroD a x ≤ WithZero.unzeroD a y
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mulPosReflectLT_iff_contravariant_pos : ∀ {α : Type u_1} [inst : MulZeroClass α] [inst_1 : PartialOrder α],
  MulPosReflectLT α ↔ ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x1 x2 => x1 < x2
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The category of additive semigroups and semigroup morphisms.  -/
AddSemigrp : Type (u + 1)
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.eventually_ge : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {f : Filter β} {u : β → α},
  Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f u → ∃ a, ∀ᶠ (x : β) in f, a ≤ u x
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.lift_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  (α : M ⟶ K) (β : CochainComplex.HomComplex.Cochain M L (-1))
  (hαβ :
    CochainComplex.HomComplex.δ (-1) 0 β +
        CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) =
      0),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCocone.lift φ α β hαβ)
      (CochainComplex.mappingCocone.fst φ) =
    α
-- Mathlib.Analysis.Normed.Module.DoubleDual
NormedSpace.dual_def : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type u_2) [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (x : E) (f : StrongDual 𝕜 E), ((NormedSpace.inclusionInDoubleDual 𝕜 E) x) f = f x
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega0_lt_preOmega_iff : ∀ {x : Ordinal.{u_1}}, Ordinal.omega0 < Ordinal.preOmega x ↔ Ordinal.omega0 < x
-- Init.Data.Ord.SInt
Int32.instLawfulOrderOrd : Std.LawfulOrderOrd Int32
-- Mathlib.Data.Real.Basic
Real.instDivInvMonoid : DivInvMonoid ℝ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.eq_of_length_eq_zero : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.length = 0 → u = v
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.WithCache.mk.inj : ∀ {α : Type u} {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} {val : α} {cache : Std.Tactic.BVDecide.BVExpr.Cache aig}
  {val_1 : α} {cache_1 : Std.Tactic.BVDecide.BVExpr.Cache aig},
  { val := val, cache := cache } = { val := val_1, cache := cache_1 } → val = val_1 ∧ cache = cache_1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonResolvableCompletionList.fromJson : Lean.Json → Except String Lean.Lsp.ResolvableCompletionList
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuousOn.lowerHemicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α}
  {s : Set α}, LowerHemicontinuousOn f s → x ∈ s → LowerHemicontinuousWithinAt f s x
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
TensorProduct.directSumRight_tmul_lof : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_1) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₂ : Type v₂}
  [inst_3 : DecidableEq ι₂] {M₁' : Type w₁'} {M₂ : ι₂ → Type w₂} [inst_4 : AddCommMonoid M₁']
  [inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [inst_6 : Module R M₁'] [inst_7 : (i₂ : ι₂) → Module R (M₂ i₂)]
  [inst_8 : Module S M₁'] [inst_9 : IsScalarTower R S M₁'] (x : M₁') (i : ι₂) (y : M₂ i),
  (TensorProduct.directSumRight R S M₁' M₂) (x ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i) y) =
    (DirectSum.lof S ι₂ (fun i => TensorProduct R M₁' (M₂ i)) i) (x ⊗ₜ[R] y)
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.dist_inversion_mul_dist_center_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c x y : P} {R : ℝ},
  x ≠ c →
    y ≠ c →
      dist (EuclideanGeometry.inversion c R x) y * dist x c = dist x (EuclideanGeometry.inversion c R y) * dist y c
-- Mathlib.Data.DFinsupp.Order
DFinsupp.support_inf : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → LinearOrder (α i)]
  [∀ (i : ι), IsBotZeroClass (α i)] [inst_3 : DecidableEq ι] {f g : Π₀ (i : ι), α i},
  (f ⊓ g).support = f.support ∩ g.support
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ShortComplex.mapToComposableArrows_app_2 : ∀ {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₂),
  (CategoryTheory.ShortComplex.mapToComposableArrows φ).app 2 = φ.τ₃
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.toSublattice : {α : Type u_2} → [inst : BooleanAlgebra α] → BooleanSubalgebra α → Sublattice α
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.add : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {c : α} [inst : Add α] [inst_1 : Add β],
  Function.Periodic f c → Function.Periodic g c → Function.Periodic (f + g) c
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.comp.get_map : ∀ {n m : ℕ} {P : MvPFunctor.{u} n} {Q : Fin2 n → MvPFunctor.{u} m} {α β : TypeVec.{u} m} (f : α.Arrow β)
  (x : ↑(P.comp Q) α),
  MvPFunctor.comp.get (MvFunctor.map f x) = MvFunctor.map (fun i x => MvFunctor.map f x) (MvPFunctor.comp.get x)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.precomposeId_inv_app_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (X : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.Cocone.precomposeId.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Init.Data.Option.Attach
Option.unattach_merge : ∀ {α : Type u_1} {p : α → Prop} {f : { x // p x } → { x // p x } → { x // p x }} {g : α → α → α},
  (∀ (x : α) (h : p x) (y : α) (h' : p y), ↑(f ⟨x, h⟩ ⟨y, h'⟩) = g x y) →
    ∀ {o o' : Option { x // p x }}, (Option.merge f o o').unattach = Option.merge g o.unattach o'.unattach
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mkAddMonoidHom.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddZeroClass M] [inst_2 : ContinuousAdd M],
  SeparationQuotient.mkAddMonoidHom = { toFun := SeparationQuotient.mk, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Order.Field.Basic
add_div_two_lt_right : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α],
  (a + b) / 2 < b ↔ a < b
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.mul_beq_mul_short_circuit_right : ∀ {w : ℕ} {x y₁ y₂ : BitVec w}, (x * y₁ == x * y₂) = !(!y₁ == y₂ && !x * y₁ == x * y₂)
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.Hom.ext : ∀ {A B : MagmaCat} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- A `Matrix m n R` is linearly equivalent to a linear map `(n → R) →ₗ[R] (m → R)`.

Note that the forward-direction does not require `DecidableEq` and is `Matrix.mulVecLin`.  -/
Matrix.toLin' : {R : Type u_1} →
  [inst : CommSemiring R] →
    {m : Type u_4} → {n : Type u_5} → [DecidableEq n] → [Fintype n] → Matrix m n R ≃ₗ[R] (n → R) →ₗ[R] m → R
-- Mathlib.Order.Completion
/-- See `DedekindCut.ext` for a version using the left set instead.  -/
DedekindCut.ext' : ∀ {α : Type u_1} [inst : Preorder α] {A B : DedekindCut α}, A.right = B.right → A = B
-- Mathlib.Analysis.Analytic.Composition
/-- If two functions `g` and `f` are analytic respectively at `f x` and `x`, within
two sets `s` and `t` such that `f` maps `s` to `t`, then `g ∘ f` is analytic at `x` within `s`.  -/
AnalyticWithinAt.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {x : E} {t : Set F} {s : Set E},
  AnalyticWithinAt 𝕜 g t (f x) → AnalyticWithinAt 𝕜 f s x → Set.MapsTo f s t → AnalyticWithinAt 𝕜 (g ∘ f) s x
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.tr.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ)
  (q : Λ), Turing.TM2to1.tr M (Turing.TM2to1.Λ'.normal q) = Turing.TM2to1.trNormal (M q)
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `μ` is inner regular for finite measure sets with respect to compact sets,
then any measurable set of finite measure can be approximated by a
compact subset. See also `MeasurableSet.exists_lt_isCompact_of_ne_top`.  -/
MeasurableSet.exists_isCompact_lt_add : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.InnerRegularCompactLTTop] ⦃A : Set α⦄,
  MeasurableSet A → μ A ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ K ⊆ A, IsCompact K ∧ μ A < μ K + ε
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_le_coe : ∀ {x y : ℝ}, ↑x ≤ ↑y ↔ x ≤ y
-- Mathlib.LinearAlgebra.StdBasis
Module.surjective_piEquiv_apply_iff : ∀ (ι : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Finite ι] [inst_1 : CommSemiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (v : ι → M),
  Function.Surjective ⇑((Module.piEquiv ι R M) v) ↔ Submodule.span R (Set.range v) = ⊤
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.instFirstCountableTopology : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] (N : AddSubgroup G)
  [FirstCountableTopology G], FirstCountableTopology (G ⧸ N)
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.intro1 : Lean.Meta.Grind.GoalM Lean.FVarId
-- Mathlib.Data.Stream.Init
Stream'.iterate.eq_def : ∀ {α : Type u} (f : α → α) (a : α) (x : ℕ),
  Stream'.iterate f a x =
    match x with
    | 0 => a
    | n.succ => f (Stream'.iterate f a n)
-- Mathlib.Tactic.Basic
Mathlib.Tactic.withResetServerInfo.Result.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (result? : Option α) (msgs : Lean.MessageLog)
  (trees : Lean.PersistentArray Lean.Elab.InfoTree),
  sizeOf { result? := result?, msgs := msgs, trees := trees } = 1 + sizeOf result? + sizeOf msgs + sizeOf trees
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_obj_obj : ∀ (b : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ),
  (AlgebraicGeometry.Scheme.Modules.pseudofunctor.obj b).obj = CategoryTheory.Cat.of (Opposite.unop b.as).Modules
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.norm_apply_le_seminorm : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {f : ContDiffMapSupportedIn E F n K}
  {x : E}, ‖f x‖ ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K 0) f
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.plusFunctor_preservesZeroMorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_4 : CategoryTheory.Preadditive D], (J.plusFunctor D).PreservesZeroMorphisms
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.instMonoPushoutInl : ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} [CategoryTheory.Mono g],
  CategoryTheory.Mono (CategoryTheory.Limits.pushout.inl f g)
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.mk.sizeOf_spec : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : LE α] [inst_2 : SizeOf α]
  (toClopens : TopologicalSpace.Clopens α) (upper' : IsUpperSet toClopens.carrier),
  sizeOf { toClopens := toClopens, upper' := upper' } = 1 + sizeOf toClopens
-- Aesop.Stats.Basic
Aesop.RuleStatsTotals.mk : ℕ → ℕ → Aesop.Nanos → Aesop.Nanos → Aesop.RuleStatsTotals
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.F_nat_one_le : ∀ {a : ℝ},
  0 ≤ a →
    ∀ {t : ℝ},
      0 < t →
        ‖HurwitzKernelBounds.F_nat 1 a t‖ ≤
          Real.exp (-Real.pi * (a ^ 2 + 1) * t) / (1 - Real.exp (-Real.pi * t)) ^ 2 +
            a * Real.exp (-Real.pi * a ^ 2 * t) / (1 - Real.exp (-Real.pi * t))
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.comp_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N K : CategoryTheory.Bimon C} (f : M ⟶ N) (g : N ⟶ K),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanDidOpenTextDocumentParams.mk : Lean.Lsp.DidOpenTextDocumentParams → Option Lean.Lsp.DependencyBuildMode → Lean.Lsp.LeanDidOpenTextDocumentParams
-- Mathlib.Data.Nat.Log
Nat.log_eq_of_pow_le_of_lt_pow : ∀ {b m n : ℕ}, b ^ m ≤ n → n < b ^ (m + 1) → Nat.log b n = m
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- The distinguished triangle `(t.truncLE n).obj A ⟶ A ⟶ (t.truncGT n).obj A ⟶ ...`
as a functor `C ⥤ Triangle C` when `t` is a t-structure on a pretriangulated
category `C` and `n : ℤ`.  -/
CategoryTheory.Triangulated.TStructure.triangleLEGT : {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] →
              CategoryTheory.Triangulated.TStructure C →
                ℤ → CategoryTheory.Functor C (CategoryTheory.Pretriangulated.Triangle C)
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of `Finset.Icc_sdiff_Ioo_self`. -/
Finset.Icc_diff_Ioo_self : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
  a ≤ b → Finset.Icc a b \ Finset.Ioo a b = {a, b}
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {fallback v : β}, (m.insert k v).getD a fallback = if (k == a) = true then v else m.getD a fallback
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ {k a : α}, (t.erase k).get? a = if cmp k a = Ordering.eq then none else t.get? a
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- The localization of a `CommMonoid` at one of its submonoids (as a quotient type).  -/
Localization : {M : Type u_1} → [inst : CommMonoid M] → Submonoid M → Type u_1
-- Lean.Data.Json.Basic
Lean.Json.getArrVal? : Lean.Json → ℕ → Except String Lean.Json
-- Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
/-- The limit of the number of nonzero integral ideals of norm `≤ s` divided by `s` when `s → +∞`.
 -/
NumberField.Ideal.tendsto_norm_le_div_atTop₀ : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Filter.Tendsto (fun s => ↑(Nat.card { I // ↑(Ideal.absNorm ↑I) ≤ s }) / s) Filter.atTop
    (nhds
      (2 ^ NumberField.InfinitePlace.nrRealPlaces K * (2 * Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
            NumberField.Units.regulator K *
          ↑(NumberField.classNumber K) /
        (↑(NumberField.Units.torsionOrder K) * √|↑(NumberField.discr K)|)))
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.vadd_eball`. -/
EMetric.vadd_ball : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [IsIsometricVAdd G X] (c : G) (x : X) (r : ENNReal), c +ᵥ Metric.eball x r = Metric.eball (c +ᵥ x) r
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.List.ProveNilOrConsResult.nil.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(List «$α»)} (pf pf_1 : Q(«$s» = [])),
  (Mathlib.Meta.List.ProveNilOrConsResult.nil pf = Mathlib.Meta.List.ProveNilOrConsResult.nil pf_1) = (pf = pf_1)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom.of.injEq : ∀ {B : Type u} [inst : Quiver B] {a b : B} (f f_1 : a ⟶ b),
  (CategoryTheory.FreeBicategory.Hom.of f = CategoryTheory.FreeBicategory.Hom.of f_1) = (f = f_1)
-- Mathlib.Algebra.Homology.Homotopy
/-- Homotopy equivalence is a transitive relation.  -/
HomotopyEquiv.trans : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D E : HomologicalComplex V c} → HomotopyEquiv C D → HomotopyEquiv D E → HomotopyEquiv C E
-- Mathlib.Data.Nat.Squarefree
Nat.minSqFac_dvd : ∀ {n d : ℕ}, n.minSqFac = some d → d * d ∣ n
-- Mathlib.Algebra.Torsor.Defs
Torsor.toSDiv : {G : outParam (Type u_1)} → {P : Type u_2} → {inst : Group G} → [self : Torsor G P] → SDiv G P
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
CompactCoherentification.continuous_dom_of_continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → Continuous (f ∘ ⇑(CompactCoherentification.mk X).symm)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, k ∉ t₂ → (t₁ \ t₂).getKey! k = t₁.getKey! k
-- Mathlib.CategoryTheory.EpiMono
/-- The section of a split epimorphism has an obvious retraction.  -/
CategoryTheory.SplitEpi.splitMono : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → {f : X ⟶ Y} → (se : CategoryTheory.SplitEpi f) → CategoryTheory.SplitMono se.section_
-- Lean.Meta.Sym.Simp.SimpM
/-- Mutable state for the simplifier.  -/
Lean.Meta.Sym.Simp.State : Type
-- Mathlib.Data.Bool.AllAny
List.any_iff_exists_prop : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {l : List α},
  (l.any fun a => decide (p a)) = true ↔ ∃ a ∈ l, p a
-- Init.Data.UInt.Lemmas
UInt16.toNat_ofNatLT : ∀ {n : ℕ} {h : n < UInt16.size}, (UInt16.ofNatLT n h).toNat = n
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.coe_dualAnnihilator_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M),
  ↑(Submodule.span R s).dualAnnihilator = {f | s ⊆ ↑f.ker}
-- Batteries.Recycling.MonadSatisfying.Basic
MonadSatisfying.satisfying.congr_simp : ∀ {m : Type u → Type v} {inst : Functor m} {inst_1 : LawfulFunctor m} [self : MonadSatisfying m] {α : Type u}
  {p : α → Prop} {x x_1 : m α} (e_x : x = x_1) (h : SatisfiesM p x), satisfying h = satisfying ⋯
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {a : α} {fallback : β},
  Std.DHashMap.Const.getD ∅ a fallback = fallback
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.restrictFunctor_obj_hom : ∀ (X : AlgebraicGeometry.Scheme) (U : X.Opens), (X.restrictFunctor.obj U).hom = U.ι
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (Y : T) (X : D)
  (Y_1 : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)),
  ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y_1).hom = Y_1.right.hom
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.of_symm_one : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ],
  (GradedTensorProduct.of R 𝒜 ℬ).symm 1 = 1
-- Init.Data.Bool
Bool.eq_true_imp_eq_false_iff : ∀ (a b : Bool), (a = true → b = false ↔ b = true → a = false) = True
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_associativity : ∀ {X Y Z T : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ T),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Modules.pullbackComp f (CategoryTheory.CategoryStruct.comp g h)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (AlgebraicGeometry.Scheme.Modules.pullbackComp g h).inv
          (AlgebraicGeometry.Scheme.Modules.pullback f))
        (CategoryTheory.CategoryStruct.comp
          ((AlgebraicGeometry.Scheme.Modules.pullback h).associator (AlgebraicGeometry.Scheme.Modules.pullback g)
              (AlgebraicGeometry.Scheme.Modules.pullback f)).hom
          (CategoryTheory.CategoryStruct.comp
            ((AlgebraicGeometry.Scheme.Modules.pullback h).whiskerLeft
              (AlgebraicGeometry.Scheme.Modules.pullbackComp f g).hom)
            (AlgebraicGeometry.Scheme.Modules.pullbackComp (CategoryTheory.CategoryStruct.comp f g) h).hom))) =
    CategoryTheory.eqToHom ⋯
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.exists_pos_eq_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] [inst_1 : LinearOrder β] [IsStrictOrderedRing β] {u v : α → β}
  {l : Filter α} [ClosedIicTopology β], Asymptotics.IsEquivalent l u v → ∃ φ, (∀ᶠ (x : α) in l, 0 < φ x) ∧ u =ᶠ[l] φ * v
-- Mathlib.Topology.Separation.Regular
regularSpace_iff : ∀ (X : Type u) [inst : TopologicalSpace X],
  RegularSpace X ↔ ∀ {s : Set X} {a : X}, IsClosed s → a ∉ s → Disjoint (nhdsSet s) (nhds a)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_eq_fallback : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α}
  {fallback : β}, a ∉ t → t.getD a fallback = fallback
-- Mathlib.Analysis.Complex.ReImTopology
Complex.closure_reProdIm : ∀ (s t : Set ℝ), closure (s ×ℂ t) = closure s ×ℂ closure t