mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Localization
ModuleCat.localizedModule_isLocalizedModule : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] (M : ModuleCat R) (S : Submonoid R),
  IsLocalizedModule S (M.localizedModuleMkLinearMap S)
-- Lean.Language.Basic
Lean.Language.ProcessingContext.mk.sizeOf_spec : ∀ (toInputContext : Lean.Parser.InputContext), sizeOf { toInputContext := toInputContext } = 1 + sizeOf toInputContext
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.coe_lsum : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} (S : Type u_8) [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring S] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : AddCommMonoid N] [inst_6 : Module R₂ N] {σ : R →+* R₂} [inst_7 : Module S N] [inst_8 : SMulCommClass R₂ S N]
  (f : α → M →ₛₗ[σ] N), ⇑((Finsupp.lsum S) f) = fun d => d.sum fun i => ⇑(f i)
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.IsDynCoverOf.of_le : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F s : Set X} {m n : ℕ},
  m ≤ n → Dynamics.IsDynCoverOf T F U n s → Dynamics.IsDynCoverOf T F U m s
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_neg : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R} [IsOrderedRing R], ⌊-a⌋ = -⌈a⌉
-- Mathlib.Analysis.Normed.Group.Basic
/-- An injective group homomorphism from an `AddGroup` to a
`NormedAddGroup` induces a `NormedAddGroup` structure on the domain.  -/
NormedAddGroup.induced : {𝓕 : Type u_1} →
  (E : Type u_5) →
    (F : Type u_6) →
      [inst : FunLike 𝓕 E F] →
        [inst_1 : AddGroup E] →
          [inst_2 : NormedAddGroup F] → [AddMonoidHomClass 𝓕 E F] → (f : 𝓕) → Function.Injective ⇑f → NormedAddGroup E
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyIso.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq' : κ) [inst_3 : X.HasSpectralSequence data],
  CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyIso X data r r' hrr' hr pq' =
    CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyIso' X data r r' hrr' hr ((c r).prev pq') pq'
      ((c r).next pq') ⋯ ⋯ (data.i₀ r' pq' ⋯) (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₂ pq') (data.i₃ r pq' ⋯)
      (data.i₃ r' pq' ⋯) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (data.deg pq' - 1) (data.deg pq') (data.deg pq' + 1) ⋯ ⋯ ⋯
-- Mathlib.RingTheory.TensorProduct.Finite
Module.Finite.tensorProduct : ∀ (R : Type u_1) (M : Type u_4) (N : Type u_5) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [hM : Module.Finite R M] [hN : Module.Finite R N],
  Module.Finite R (TensorProduct R M N)
-- Init.Data.String.Lemmas.Basic
String.append_eq_right_iff : ∀ {s t : String}, s ++ t = t ↔ s = ""
-- Mathlib.Util.WhatsNew
Mathlib.WhatsNew.diffExtension : Lean.Environment →
  Lean.Environment →
    Lean.PersistentEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState →
      Lean.CoreM (Option Lean.MessageData)
-- Mathlib.Algebra.Group.Prod
Prod.addSemiconjBy_iff : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N] {x y z : M × N},
  AddSemiconjBy x y z ↔ AddSemiconjBy x.1 y.1 z.1 ∧ AddSemiconjBy x.2 y.2 z.2
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
nndist_ofAdd : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] (a b : X),
  nndist (Multiplicative.ofAdd a) (Multiplicative.ofAdd b) = nndist a b
-- Mathlib.Topology.Separation.Hausdorff
/-- If two continuous functions are equal on a dense set, then they are equal.  -/
Continuous.ext_on : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space X] {s : Set Y},
  Dense s → ∀ {f g : Y → X}, Continuous f → Continuous g → Set.EqOn f g s → f = g
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_divLeft_nhds : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {c a : G},
  Filter.map (fun x => c / x) (nhds a) = nhds (c / a)
-- Mathlib.Topology.Sets.BaseChangeNhds
/-- For `U` an open subset included in a open subset `V`, there is
a map sending compacts inside `U` to the ones inside `V`  -/
TopologicalSpace.Opens.baseChangeCompactsInside : {α : Type u_1} →
  [inst : TopologicalSpace α] → {U V : TopologicalSpace.Opens α} → (U ⟶ V) → ↑U.compactsInside → ↑V.compactsInside
-- Mathlib.Algebra.BigOperators.Ring.Multiset
Multiset.sum_map_mul_left : ∀ {ι : Type u_1} {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] {a : R} {s : Multiset ι} {f : ι → R},
  (Multiset.map (fun i => a * f i) s).sum = a * (Multiset.map f s).sum
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.IsClosedUnderBinaryProducts.closedUnderIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.Limits.HasTerminal C] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [P.IsClosedUnderBinaryProducts], P.IsClosedUnderIsomorphisms
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_ofNatLT : ∀ {n : ℕ} (hn : n < UInt16.size), (UInt16.ofNatLT n hn).toBitVec = n#'hn
-- Mathlib.Logic.Function.Basic
Function.Bijective.of_comp_iff' : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
  Function.Bijective f → ∀ (g : γ → α), Function.Bijective (f ∘ g) ↔ Function.Bijective g
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.mem_alterKey_of_key_not_beq : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {a : α} {f : Option β → Option β} {l : List ((_ : α) × β)}
  (p : (_ : α) × β), (p.fst == a) = false → (p ∈ Std.Internal.List.Const.alterKey a f l ↔ p ∈ l)
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.oneHomClass : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N], OneHomClass (OneHom M N) M N
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.transversal_nonempty : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  (φ : (i : ι) → H →* G i), (∀ (i : ι), Function.Injective ⇑(φ i)) → Nonempty (Monoid.PushoutI.NormalWord.Transversal φ)
-- Lean.Environment
/-- If `enabled = true`, kernel records declarations that have been unfolded.  -/
Lean.Kernel.Diagnostics.enabled : Lean.Kernel.Diagnostics → Bool
-- Mathlib.Data.Finset.Lattice.Fold
/-- Supremum of a finite set: `sup {a, b, c} f = f a ⊔ f b ⊔ f c`  -/
Finset.sup : {α : Type u_2} → {β : Type u_3} → [inst : SemilatticeSup α] → [OrderBot α] → Finset β → (β → α) → α
-- Mathlib.Data.Set.Order
/-- **Alias** of `Set.monotone_ofPred`. -/
Set.monotone_setOf : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {p : α → β → Prop},
  (∀ (b : β), Monotone fun a => p a b) → Monotone fun a => {b | p a b}
-- Init.Data.UInt.Bitwise
USize.shiftLeft_xor : ∀ {a b c : USize}, (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_sq_eq_def : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, ‖z‖ ^ 2 = RCLike.re z * RCLike.re z + RCLike.im z * RCLike.im z
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_mk : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Subsemiring A)
  (h : ∀ (r : R), (algebraMap R A) r ∈ s.carrier), ↑{ toSubsemiring := s, algebraMap_mem' := h } = ↑s
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
/-- The multiplicity of an irreducible factor of a nonzero element is exactly the number of times
the normalized factor occurs in the `normalizedFactors`.

For a version using `emultiplicity`, see `emultiplicity_eq_count_normalizedFactors`.  -/
UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R] [inst_2 : NormalizationMonoid R]
  [inst_3 : DecidableEq R] {a b : R},
  Irreducible a →
    b ≠ 0 → multiplicity a b = Multiset.count (normalize a) (UniqueFactorizationMonoid.normalizedFactors b)
-- Lean.Expr
/-- Returns `let x : t := v; b`, a `let` expression. If `nondep := true`, then returns a `have`.  -/
Lean.mkLet : Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr → optParam Bool false → Lean.Expr
-- Mathlib.Topology.Algebra.Field
IsTopologicalDivisionRing.mk : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : TopologicalSpace K] [toIsTopologicalRing : IsTopologicalRing K]
  [toContinuousInv₀ : ContinuousInv₀ K], IsTopologicalDivisionRing K
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocDeclExtState.mk.injEq : ∀ (builtin : Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey))
  (newEntries : Lean.PHashMap Lean.Name (Array Lean.Meta.SimpTheoremKey))
  (builtin_1 : Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey))
  (newEntries_1 : Lean.PHashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)),
  ({ builtin := builtin, newEntries := newEntries } = { builtin := builtin_1, newEntries := newEntries_1 }) =
    (builtin = builtin_1 ∧ newEntries = newEntries_1)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The isomorphism (in `Type`) between
morphisms from a specified object `W` to the limit object,
and an explicit componentwise description of cones with cone point `W`.
 -/
CategoryTheory.Limits.limit.homIso' : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            (W : C) →
              ULift.{u₁, v} (W ⟶ CategoryTheory.Limits.limit F) ≅
                { p // ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (p j) (F.map f) = p j' }
-- Std.Data.DHashMap.Raw
/-- Returns a list of all values present in the hash map in some order.  -/
Std.DHashMap.Raw.values : {α : Type u} → {β : Type v} → (Std.DHashMap.Raw α fun x => β) → List β
-- Mathlib.LinearAlgebra.Projectivization.PSL.PSL2
/-- A transvection `transvection i j hij b` lies in `lineStab (span F {Pi.single i 1})`.  -/
SL2Gen.transvection_mem_lineStab : ∀ {ι : Type u_1} {F : Type u_2} [inst : Field F] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {i j : ι} (hij : i ≠ j)
  (b : F), Matrix.SpecialLinearGroup.transvection hij b ∈ Matrix.SpecialLinearGroup.lineStab (F ∙ Pi.single i 1)
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndepOn.id_imageₛ : ∀ {R : Type u_2} {M : Type u_4} {M' : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] {s : Set M} {f : M →ₗ[R] M'},
  LinearIndepOn R id s → Set.InjOn ⇑f ↑(Submodule.span R s) → LinearIndepOn R id (⇑f '' s)
-- Mathlib.Analysis.Convex.PathConnected
/-- A nonempty convex set is connected.  -/
Convex.isConnected : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E] {s : Set E}, Convex ℝ s → s.Nonempty → IsConnected s
-- Mathlib.Analysis.Complex.Exponential
Real.exp_nsmul : ∀ (x : ℝ) (n : ℕ), Real.exp (n • x) = Real.exp x ^ n
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.mk.injEq : ∀ {n : ℕ} (parts : Multiset ℕ) (parts_pos : ∀ {i : ℕ}, i ∈ parts → 0 < i) (parts_sum : parts.sum = n)
  (parts_1 : Multiset ℕ) (parts_pos_1 : ∀ {i : ℕ}, i ∈ parts_1 → 0 < i) (parts_sum_1 : parts_1.sum = n),
  ({ parts := parts, parts_pos := parts_pos, parts_sum := parts_sum } =
      { parts := parts_1, parts_pos := parts_pos_1, parts_sum := parts_sum_1 }) =
    (parts = parts_1)
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.isTopologicalSpace : (self : TopCommRingCat) → TopologicalSpace self.α
-- Lean.Meta.Basic
Lean.Meta.modifyInferTypeCache : (Lean.Meta.InferTypeCache → Lean.Meta.InferTypeCache) → Lean.MetaM Unit
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaKey.mk : Lean.Expr → Lean.Meta.Sym.AlphaKey
-- Init.Data.List.MinMaxOn
List.maxOn?_cons_eq_some_maxOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x : α} {xs : List α},
  List.maxOn? f (x :: xs) = some (List.maxOn f (x :: xs) ⋯)
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.instHasProjectiveDimensionLTHAddNat_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C) (n : ℕ)
  [CategoryTheory.HasProjectiveDimensionLT X n] (k : ℕ), CategoryTheory.HasProjectiveDimensionLT X (k + n)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.nodup_toList : ∀ {α : Type u} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.Rxi.IsAlwaysFinite α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α], *...*.toList.Nodup
-- Lean.Parser.Tactic.Doc
/-- Finds the custom name assigned to `tac`, or returns `none` if there is no such custom name.
 -/
Lean.Parser.Tactic.Doc.customTacticName : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (Option String)
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The source of the arrow.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.Y : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → {S : J.Cover X} → S.Arrow → C
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∈ m₁ ∪ m₂ → k ∉ m₁ → k ∈ m₂
-- Mathlib.Topology.Order.DenselyOrdered
/-- If the order topology for a dense linear ordering is discrete, the space has at most one point.

We would prefer for this to be an instance but even at `(priority := 100)` this was problematic so
we have deferred this issue. TODO Promote this to an `instance`!  -/
DenselyOrdered.subsingleton_of_discreteTopology : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [DiscreteTopology α], Subsingleton α
-- Lean.Elab.MutualInductive
/-- A view for generic inductive types.  -/
Lean.Elab.Command.InductiveView : Type
-- Mathlib.Topology.Algebra.Group.Basic
instIsTopologicalAddGroupAdditiveOfIsTopologicalGroup : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G],
  IsTopologicalAddGroup (Additive G)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.top_ne_ofNat : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ) [inst_1 : n.AtLeastTwo], ⊤ ≠ OfNat.ofNat n
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If a T1 group acts properly on a topological space, then this topological space is T2.  -/
t2Space_of_properSMul_of_t1Group : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [h_proper : ProperSMul G X] [T1Space G], T2Space X
-- Mathlib.Logic.Equiv.PartialEquiv
/-- The identity partial equivalence on a set `s`  -/
PartialEquiv.ofSet : {α : Type u_1} → Set α → PartialEquiv α α
-- Mathlib.Algebra.Group.Action.Defs
IsCancelSMul.right_cancel : ∀ {G : Type u_11} {P : Type u_12} [inst : SMul G P] [IsCancelSMul G P] (a b : G) (c : P), a • c = b • c → a = b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {aig : Std.Sat.AIG α} {len : ℕ}
  (x x_1 : aig.RefVec (len * w)),
  x = x_1 →
    ∀ (h : 0 < len),
      Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go x h =
        Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go x_1 h
-- Init.Prelude
AndOp.mk : {α : Type u} → (α → α → α) → AndOp α
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_insertListIfNewUnit_of_contains_eq_false_of_mem : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k k' fallback : α},
  (k == k') = true →
    Std.Internal.List.containsKey k l = false →
      List.Pairwise (fun a b => (a == b) = false) toInsert →
        k ∈ toInsert → Std.Internal.List.getKeyD k' (Std.Internal.List.insertListIfNewUnit l toInsert) fallback = k
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
/-- To show a property is true on the odd parts, it suffices to show it is true on the
vectors, closed under addition, and under left-multiplication by a pair of vectors.  -/
CliffordAlgebra.odd_induction : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) {P : (x : CliffordAlgebra Q) → x ∈ CliffordAlgebra.evenOdd Q 1 → Prop},
  (∀ (v : M), P ((CliffordAlgebra.ι Q) v) ⋯) →
    (∀ (x y : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 1) (hy : y ∈ CliffordAlgebra.evenOdd Q 1),
        P x hx → P y hy → P (x + y) ⋯) →
      (∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 1),
          P x hx → P ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯) →
        ∀ (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 1), P x hx
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_erase_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {fallback : β k},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.getD k fallback = fallback
-- Lean.Meta.Tactic.Grind.EqResolution
Lean.Meta.Grind.TopSort.State.mk.sizeOf_spec : ∀ (tempMark permMark : Std.HashSet Lean.Expr) (result : Array Lean.Expr),
  sizeOf { tempMark := tempMark, permMark := permMark, result := result } =
    1 + sizeOf tempMark + sizeOf permMark + sizeOf result
-- Lean.SubExpr
/-- The position of the subexpression within the root expression.  -/
Lean.SubExpr.pos : Lean.SubExpr → Lean.SubExpr.Pos
-- Mathlib.Algebra.BigOperators.Finprod
/-- **Alias** of `one_lt_finprod`. -/
one_lt_finprod' : ∀ {ι : Type u_3} {M : Type u_7} [inst : CommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M},
  (∀ (i : ι), 1 ≤ f i) → (∃ i, 1 < f i) → Function.HasFiniteMulSupport f → 1 < ∏ᶠ (i : ι), f i
-- Init.Meta.Defs
/-- Remove macros scopes, apply `f`, and put them back  -/
Lean.Name.modifyBase : Lean.Name → (Lean.Name → Lean.Name) → Lean.Name
-- Std.Time.Time.Unit.Millisecond
/-- Creates an `Offset` from an integer.
 -/
Std.Time.Millisecond.Offset.ofInt : ℤ → Std.Time.Millisecond.Offset
-- Mathlib.Topology.MetricSpace.Holder
/-- If a function is `(C, r)`-Hölder and `(C, s)`-Hölder,
then it is `(C, r * t₁ + s * t₂)`-Hölder for all `t₁ t₂ : ℝ≥0` such that
`t₁ + t₂ = 1`.  -/
HolderOnWith.interpolate_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {C s t₁ t₂ : NNReal} {A : Set X},
  HolderOnWith C r f A → HolderOnWith C s f A → t₁ + t₂ = 1 → HolderOnWith C (r * t₁ + s * t₂) f A
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_unsat_coeff_cert.eq_1 : ∀ (p : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.eq_unsat_coeff_cert p k =
    (Int.Internal.Linear.Poly.divCoeffs k p).and'
      ((Int.blt' 0 k).and' (decide (Int.Internal.Linear.cmod p.getConst k < 0)))
-- Mathlib.Algebra.Group.TypeTags.Hom
MonoidHom.toAdditiveRight_symm_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : AddZeroClass α] [inst_1 : MulOneClass β] (a : α →+ Additive β)
  (a_1 : Multiplicative α), (MonoidHom.toAdditiveRight.symm a) a_1 = Additive.toMul (a (Multiplicative.toAdd a_1))
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_of_nonpos : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], a ≤ 0 → |a| = -a
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.range_logb : ∀ {b : ℝ}, 0 < b → b ≠ 1 → Set.range (Real.logb b) = Set.univ
-- Lean.Meta.NatTable
_private.Lean.Meta.NatTable.0.Lean.mkNatLookupTable.go.eq_def : ∀ (i type : Lean.Expr) (es : Array Lean.Expr) (u : Lean.Level) (start stop : ℕ) (hstart : start < stop)
  (hstop : stop ≤ es.size),
  Lean.mkNatLookupTable.go✝ i type es u start stop hstart hstop =
    if h : start + 1 = stop then pure es[start]
    else
      let mid := (start + stop) / 2;
      do
      let low ← Lean.mkNatLookupTable.go✝ i type es u start mid ⋯ ⋯
      let high ← Lean.mkNatLookupTable.go✝ i type es u mid stop ⋯ hstop
      pure
          (Lean.mkApp4 (Lean.mkConst `cond [u]) type
            (Lean.mkApp2 (Lean.mkConst `Nat.ble) i (Lean.mkRawNatLit (mid - 1))) low high)
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.merge.match_3.eq_3 : ∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α → Sort u_2) (r₁ : ℕ)
  (a₁ : α) (n₁ : Batteries.BinomialHeap.Imp.HeapNode α) (t₁ : Batteries.BinomialHeap.Imp.Heap α) (r₂ : ℕ) (a₂ : α)
  (n₂ : Batteries.BinomialHeap.Imp.HeapNode α) (t₂ : Batteries.BinomialHeap.Imp.Heap α)
  (h_1 : (h : Batteries.BinomialHeap.Imp.Heap α) → motive Batteries.BinomialHeap.Imp.Heap.nil h)
  (h_2 : (h : Batteries.BinomialHeap.Imp.Heap α) → motive h Batteries.BinomialHeap.Imp.Heap.nil)
  (h_3 :
    (s₁ : Batteries.BinomialHeap.Imp.Heap α) →
      (r₁ : ℕ) →
        (a₁ : α) →
          (n₁ : Batteries.BinomialHeap.Imp.HeapNode α) →
            (t₁ : Batteries.BinomialHeap.Imp.Heap α) →
              s₁ = Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁ →
                (s₂ : Batteries.BinomialHeap.Imp.Heap α) →
                  (r₂ : ℕ) →
                    (a₂ : α) →
                      (n₂ : Batteries.BinomialHeap.Imp.HeapNode α) →
                        (t₂ : Batteries.BinomialHeap.Imp.Heap α) →
                          s₂ = Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂ →
                            motive (Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁)
                              (Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂)),
  (match Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁, Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂ with
    | Batteries.BinomialHeap.Imp.Heap.nil, h => h_1 h
    | h, Batteries.BinomialHeap.Imp.Heap.nil => h_2 h
    | s₁@h:(Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁),
      s₂@h_4:(Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂) => h_3 s₁ r₁ a₁ n₁ t₁ h s₂ r₂ a₂ n₂ t₂ h_4) =
    h_3 (Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁) r₁ a₁ n₁ t₁ ⋯
      (Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂) r₂ a₂ n₂ t₂ ⋯
-- Init.Data.SInt.Lemmas
Int32.ofNat_toNatClampNeg : ∀ (x : Int32), 0 ≤ x → Int32.ofNat x.toNatClampNeg = x
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.eq_bot_or_nonempty : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (Q : AffineSubspace k P), Q = ⊥ ∨ (↑Q).Nonempty
-- Mathlib.Algebra.GroupWithZero.Units.Basic
mul_div_cancel_left_of_imp : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {a b : G₀}, (a = 0 → b = 0) → a * b / a = b
-- Mathlib.Topology.Order.OrderClosed
Filter.Tendsto.eventually_const_lt : ∀ {α : Type u} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {l : Filter γ}
  {f : γ → α} {u v : α}, u < v → Filter.Tendsto f l (nhds v) → ∀ᶠ (a : γ) in l, u < f a
-- Mathlib.Analysis.Normed.Lp.ProdLp
IsometryEquiv.withLpProdCongr_symm_apply : ∀ (p : ENNReal) {α : Type u_2} {β : Type u_3} {α' : Type u_5} {β' : Type u_6} [hp : Fact (1 ≤ p)]
  [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] [inst_2 : PseudoEMetricSpace α']
  [inst_3 : PseudoEMetricSpace β'] (f : α ≃ᵢ α') (g : β ≃ᵢ β') (a : WithLp p (α' × β')),
  (IsometryEquiv.withLpProdCongr p f g).symm a = WithLp.toLp p (Prod.map (⇑f.symm) (⇑g.symm) a.ofLp)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_empty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α}, ∅.size = 0