mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
/-- If a nonempty ball in a proper space includes a closed set `s`, then there exists a nonempty
ball with the same center and a strictly smaller radius that includes `s`.  -/
exists_pos_lt_subset_ball : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [ProperSpace α] {x : α} {r : ℝ} {s : Set α},
  0 < r → IsClosed s → s ⊆ Metric.ball x r → ∃ r' ∈ Set.Ioo 0 r, s ⊆ Metric.ball x r'
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.add_mul_right_left_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime (x + z * y) y ↔ IsCoprime x y
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv.go.induct_unfolding : ∀ (n : ℕ) (motive : (p : ℕ) → 1 < p ∧ n ≠ 0 → ℕ × ℕ → Prop),
  (∀ (p : ℕ) (hp : 1 < p ∧ n ≠ 0),
      n % p = 0 →
        ∀ (e q : ℕ),
          Nat.maxPowDvdDiv.go n (p * p) ⋯ = (e, q) →
            q % p = 0 → motive (p * p) ⋯ (Nat.maxPowDvdDiv.go n (p * p) ⋯) → motive p hp (2 * e + 1, q / p)) →
    (∀ (p : ℕ) (hp : 1 < p ∧ n ≠ 0),
        n % p = 0 →
          ∀ (e q : ℕ),
            Nat.maxPowDvdDiv.go n (p * p) ⋯ = (e, q) →
              ¬q % p = 0 → motive (p * p) ⋯ (Nat.maxPowDvdDiv.go n (p * p) ⋯) → motive p hp (2 * e, q)) →
      (∀ (p : ℕ) (hp : 1 < p ∧ n ≠ 0), ¬n % p = 0 → motive p hp (0, n)) →
        ∀ (p : ℕ) (hp : 1 < p ∧ n ≠ 0), motive p hp (Nat.maxPowDvdDiv.go n p hp)
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.ReflexiveRelation.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} →
      {p₁ p₂ : R ⟶ X} →
        CategoryTheory.JointlyMono₂ p₁ p₂ →
          (r : X ⟶ R) →
            autoParam (CategoryTheory.CategoryStruct.comp r p₁ = CategoryTheory.CategoryStruct.id X)
                CategoryTheory.ReflexiveRelation.reflexivity₁._autoParam →
              autoParam (CategoryTheory.CategoryStruct.comp r p₂ = CategoryTheory.CategoryStruct.id X)
                  CategoryTheory.ReflexiveRelation.reflexivity₂._autoParam →
                CategoryTheory.ReflexiveRelation p₁ p₂
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The forgetful functor from
additive commutative monoids to additive monoids preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of additive
monoids.  -/
AddCommMonCat.forget₂AddMonPreservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1}
    (CategoryTheory.forget₂ AddCommMonCat AddMonCat)
-- Mathlib.RingTheory.HahnSeries.Summable
/-- A summable family given by pointwise multiplication of a pair of summable families.  -/
HahnSeries.SummableFamily.mul : {Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} →
      {β : Type u_6} →
        [inst : AddCommMonoid Γ] →
          [inst_1 : PartialOrder Γ] →
            [IsOrderedCancelAddMonoid Γ] →
              [inst : Semiring R] →
                HahnSeries.SummableFamily Γ R α →
                  HahnSeries.SummableFamily Γ R β → HahnSeries.SummableFamily Γ R (α × β)
-- Mathlib.Computability.DFA
DFA.eval_append_singleton : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) (x : List α) (a : α), M.eval (x ++ [a]) = M.step (M.eval x) a
-- Mathlib.Topology.Constructions.SumProd
IsClosedMap.sumElim : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z}, IsClosedMap f → IsClosedMap g → IsClosedMap (Sum.elim f g)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.adjoint_toSpanSingleton : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (x : E),
  ContinuousLinearMap.adjoint (ContinuousLinearMap.toSpanSingleton 𝕜 x) = (innerSL 𝕜) x
-- Lean.Meta.Tactic.Grind.Split
/-- Returns `true` if the given list can be compressed using `<;>` at `splitCore`  -/
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.Action.isCompressibleSeq : List (Lean.TSyntax `grind) → Bool
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.neighborSet_iSup : ∀ {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ι → G.Subgraph) (v : V),
  (⨆ i, f i).neighborSet v = ⋃ i, (f i).neighborSet v
-- Mathlib.Data.Finset.Lattice.Basic
Finset.notMem_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∉ s ∪ t ↔ a ∉ s ∧ a ∉ t
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE_app_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) (a b : ℤ) (h : a ≤ b) (X : C),
  ((CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE✝ t a b h).app X).hom₂ =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Hom.addGroup.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G X : C}
  [inst_2 : CategoryTheory.AddGrpObj G],
  CategoryTheory.Hom.addGroup =
    { toAddMonoid := CategoryTheory.Hom.addMonoid,
      neg := fun f => CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg, sub := SubNegMonoid.sub',
      zsmul := zsmulRec, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β},
  k ∉ m₂ → Std.ExtDHashMap.Const.getD (m₁ ∩ m₂) k fallback = fallback
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (n : ℕ) (X : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ),
  (CategoryTheory.ComposableArrows.opEquivalence C n).unitIso.inv.app X =
    CategoryTheory.CategoryStruct.comp
      ((⋯.functor.comp (CategoryTheory.orderDualEquivalence (Fin (n + 1))).functor).whiskerLeft
          (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).inverse.comp ⋯.functor).comp
                    (Opposite.unop X)).rightOpLeftOpIso.inv.op.unop).op
      (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.funInvIdAssoc
            (Opposite.unop X)).inv.op
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdSndIsoProd_inv_fst_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Z Y] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Z X]
  [inst_3 : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdSndIsoProd f Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.prod.snd f)
        CategoryTheory.Limits.prod.snd) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd f
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Ico_sub_one_right_eq_Ico : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] {a b : α},
  a < b → insert (b - 1) (Set.Ico a (b - 1)) = Set.Ico a b
-- Init.Data.UInt.Lemmas
UInt8.mod_def : ∀ (a b : UInt8), a % b = { toBitVec := a.toBitVec % b.toBitVec }
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.mk.inj : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  {inst_3 : AddCommGroup M} {inst_4 : Module R M} {inst_5 : LieRingModule L M} {inst_6 : LieModule R L M}
  {toLinearMap : L →ₗ[R] M} {leibniz' : ∀ (a b : L), toLinearMap ⁅a, b⁆ = ⁅a, toLinearMap b⁆ - ⁅b, toLinearMap a⁆}
  {toLinearMap_1 : L →ₗ[R] M}
  {leibniz'_1 : ∀ (a b : L), toLinearMap_1 ⁅a, b⁆ = ⁅a, toLinearMap_1 b⁆ - ⁅b, toLinearMap_1 a⁆},
  { toLinearMap := toLinearMap, leibniz' := leibniz' } = { toLinearMap := toLinearMap_1, leibniz' := leibniz'_1 } →
    toLinearMap = toLinearMap_1
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α]
  [inst : Inhabited γ] {f : α → β → γ} {k : α}, (Std.HashMap.map f m)[k]! = (Option.map (f k) m[k]?).get!
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.instLinearOrder : {K : Type u_1} →
  [inst : LinearOrder K] →
    [inst_1 : Field K] → [inst_2 : IsOrderedRing K] → LinearOrder (ArchimedeanClass.FiniteResidueField K)
-- Mathlib.Topology.Instances.CantorSet
preCantorSet.eq_2 : ∀ (n : ℕ), preCantorSet n.succ = (fun x => x / 3) '' preCantorSet n ∪ (fun x => (2 + x) / 3) '' preCantorSet n
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommFold.eq_1 : ∀ {α : Type u_3} (op : α → α → α) [assoc : Std.Associative op] (s : Multiset α)
  (comm : {x | x ∈ s}.Pairwise fun x y => op x y = op y x),
  Multiset.noncommFold op s comm = Multiset.noncommFoldr op s ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The shape of a multiequalizer diagram. It involves two types `L` and `R`,
and two maps `R → L`.  -/
CategoryTheory.Limits.MulticospanShape : Type (max (w + 1) (w' + 1))
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.ker_fst_of_isClosedImmersion : ∀ {X Y Z : AlgebraicGeometry.Scheme} (i : Z ⟶ Y) (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion i],
  AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Limits.pullback.fst f i) =
    (AlgebraicGeometry.Scheme.Hom.ker i).comap f
-- Init.GetElem
/-- The syntax `arr[i]!` gets the `i`'th element of the collection `arr`,
if it is present, and otherwise panics at runtime and returns the `default` term
from `Inhabited elem`.


Conventions for notations in identifiers:

 * The recommended spelling of `xs[i]!` in identifiers is `getElem!`. -/
GetElem?.getElem! : {coll : Type u} →
  {idx : Type v} →
    {elem : outParam (Type w)} →
      {valid : outParam (coll → idx → Prop)} →
        [self : GetElem? coll idx elem valid] → [Inhabited elem] → coll → idx → elem
-- Init.Data.String.Termination
String.Slice.Pos.remainingBytes_inj : ∀ {s : String.Slice} {p q : s.Pos}, p.remainingBytes = q.remainingBytes ↔ p = q
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.instTop : {ι : Type u_1} → Top (AbstractSimplicialComplex ι)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instAddCommGroupWithOne : {R : Type u_3} → {c₁ c₂ c₃ : R} → [AddCommGroupWithOne R] → AddCommGroupWithOne (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.hom_inv_s₀_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  (i : E.I₀), e.inv.s₀ (e.hom.s₀ i) = i
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_iff_exists_mul' : ∀ {α : Type u} [inst : CommMagma α] [inst_1 : Preorder α] [CanonicallyOrderedMul α] {a b : α}, a ≤ b ↔ ∃ c, b = c * a
-- Mathlib.RingTheory.Nakayama
/-- **Nakayama's Lemma** - Statement (8) in
[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV).

If `N` is a finitely generated `R`-submodule of `M`,
`I` is an ideal contained in the Jacobson radical of `R`,
`s` is a set of `M / (I • N)` that spans the quotient image of `N`,
then there exists a spanning set `t` of `N` in bijection with `s` via the quotient map.
 -/
Submodule.exists_injOn_mkQ_image_span_eq_of_span_eq_map_mkQ_of_le_jacobson_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {N : Submodule R M} (s : Set (M ⧸ I • N)),
  N.FG →
    I ≤ ⊥.jacobson →
      Submodule.span R s = Submodule.map (I • N).mkQ N →
        ∃ t, Set.InjOn (⇑(I • N).mkQ) t ∧ ⇑(I • N).mkQ '' t = s ∧ Submodule.span R t = N
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- A covariant derivative ∇ is called of class `C^k` iff, whenever `X` is a `C^k` section and `σ` a
`C^{k+1}` section, the result `∇_X σ` is a `C^k` section. This is a class so typeclass inference can
deduce this automatically. We will prove in a later file that any `C^(k+1)` covariant derivative
is `C^k`.
 -/
ContMDiffCovariantDerivativeOn : {𝕜 : 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] →
                      (F : Type u_5) →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [inst_14 : FiberBundle F V] →
                                            [IsManifold I 1 M] →
                                              [VectorBundle 𝕜 F V] →
                                                WithTop ℕ∞ →
                                                  (((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x) →
                                                    Set M → Prop
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.isUnit_leadingCoeff_mul_left_eq_zero_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, IsUnit p.leadingCoeff → ∀ {q : Polynomial R}, q * p = 0 ↔ q = 0
-- Mathlib.Algebra.Ring.Equiv
MulEquiv.isRightCancelMulZero_iff : ∀ {A : Type u_7} {B : Type u_8} [inst : MulZeroClass A] [inst_1 : MulZeroClass B] (e : A ≃* B),
  IsRightCancelMulZero A ↔ IsRightCancelMulZero B
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.coindep_def : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.Coindep X ↔ M✶.Indep X
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.eqToHom_codomain_lift_id : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  {p : CategoryTheory.Functor 𝒳 𝒮} {a b : 𝒳} (hab : a = b) {S : 𝒮},
  p.obj b = S → p.IsHomLift (CategoryTheory.CategoryStruct.id S) (CategoryTheory.eqToHom hab)
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddRightCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddLeftCancelMonoid α],
  AddOpposite.instAddRightCancelMonoid = { toAddMonoid := AddOpposite.instAddMonoid, toIsRightCancelAdd := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- An additive submonoid `S` includes `closure s` if and only if it includes `s`.  -/
AddSubmonoid.closure_le : ∀ {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {S : AddSubmonoid M}, AddSubmonoid.closure s ≤ S ↔ s ⊆ ↑S
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.ofList_singleton : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {k : α} {v : β k},
  Std.DTreeMap.Raw.ofList [⟨k, v⟩] cmp = ∅.insert k v
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.size_balanceL! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  l.Balanced →
    r.Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size →
        (Std.DTreeMap.Internal.Impl.balanceL! k v l r).size = l.size + 1 + r.size
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_ite : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] {s : Finset ι} {p : ι → Prop} [inst_1 : DecidablePred p]
  (f g : ι → M), (∏ x ∈ s, if p x then f x else g x) = (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, g x
-- Mathlib.Data.Num.Lemmas
PosNum.distrib : Distrib PosNum
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation
/-- Given `f : ℂ → ℂ` and `R : ℝ`, define the Cartan kernel of integration as the function
`α β ↦ log ‖f (circleMap 0 R β) - circleMap 0 1 α‖`.
 -/
ValueDistribution.Cartan.cartanKernel : (ℂ → ℂ) → ℝ → ℝ → ℝ → ℝ
-- Lean.Compiler.ExternAttr
Lean.instBEqExternEntry : BEq Lean.ExternEntry
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.isFinitePlace_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (v : AbsoluteValue K ℝ),
  NumberField.IsFinitePlace v ↔ ∃ w, ↑w = v
-- Mathlib.Algebra.Ring.Ext
NonUnitalNonAssocRing.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : NonUnitalNonAssocRing R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopicRel.trans : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {S : Set X} ⦃f g h : C(X, Y)⦄,
  f.HomotopicRel g S → g.HomotopicRel h S → f.HomotopicRel h S
-- Mathlib.Topology.Metrizable.Uniformity
PseudoMetricSpace.dist_ofPreNNDist : ∀ {X : Type u_1} (d : X → X → NNReal) (dist_self : ∀ (x : X), d x x = 0) (dist_comm : ∀ (x y : X), d x y = d y x)
  (x y : X), dist x y = ↑(⨅ l, (List.zipWith d (x :: l) (l ++ [y])).sum)
-- Mathlib.Order.UpperLower.Principal
LowerSet.map_Iio : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (a : α),
  (LowerSet.map f) (LowerSet.Iio a) = LowerSet.Iio (f a)
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.exists_eq_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [PreconnectedSpace X] [Nonempty Y]
  (f : LocallyConstant X Y), ∃ y, f = LocallyConstant.const X y
-- Mathlib.Tactic.FunProp.ToBatteries
_private.Mathlib.Tactic.FunProp.ToBatteries.0.Mathlib.Meta.FunProp.betaThroughLetAux.match_1.splitter : (motive : Lean.Expr → List Lean.Expr → Sort u_1) →
  (f : Lean.Expr) →
    (args : List Lean.Expr) →
      ((f : Lean.Expr) → motive f []) →
        ((binderName : Lean.Name) →
            (binderType b : Lean.Expr) →
              (binderInfo : Lean.BinderInfo) →
                (a : Lean.Expr) →
                  (as : List Lean.Expr) → motive (Lean.Expr.lam binderName binderType b binderInfo) (a :: as)) →
          ((n : Lean.Name) →
              (t v b : Lean.Expr) →
                (nondep : Bool) →
                  (args : List Lean.Expr) → (args = [] → False) → motive (Lean.Expr.letE n t v b nondep) args) →
            ((data : Lean.MData) →
                (b : Lean.Expr) →
                  (args : List Lean.Expr) → (args = [] → False) → motive (Lean.Expr.mdata data b) args) →
              ((f : Lean.Expr) →
                  (args : List Lean.Expr) →
                    (args = [] → False) →
                      (∀ (binderName : Lean.Name) (binderType b : Lean.Expr) (binderInfo : Lean.BinderInfo)
                          (a : Lean.Expr) (as : List Lean.Expr),
                          f = Lean.Expr.lam binderName binderType b binderInfo → args = a :: as → False) →
                        (∀ (n : Lean.Name) (t v b : Lean.Expr) (nondep : Bool),
                            f = Lean.Expr.letE n t v b nondep → False) →
                          (∀ (data : Lean.MData) (b : Lean.Expr), f = Lean.Expr.mdata data b → False) → motive f args) →
                motive f args
-- Batteries.Lean.Except
_private.Batteries.Lean.Except.0.ExceptT.bindCont.match_1.eq_2 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (e : ε) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.error e with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_2 e
-- Mathlib.Algebra.Homology.Augment
_private.Mathlib.Algebra.Homology.Augment.0.ChainComplex.augment.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (i : ℕ) → motive i.succ),
  (match 0 with
    | 0 => h_1 ()
    | i.succ => h_2 i) =
    h_1 ()
-- Mathlib.CategoryTheory.Core
/-- A functor `C ⥤ D` induces a functor `Core C ⥤ Core D`.  -/
CategoryTheory.Functor.core : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.Functor (CategoryTheory.Core C) (CategoryTheory.Core D)
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- When `K` is a cochain complex indexed by `ℤ`, this is the isomorphism
`(K.truncLE n).X n ≅ K.cycles n`.  -/
CochainComplex.truncLEXIsoCycles : {C : Type u_2} →
  [inst : CategoryTheory.Category.{u_3, u_2} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        (K : CochainComplex C ℤ) →
          [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] →
            (n : ℤ) → (K.truncLE n).X n ≅ HomologicalComplex.cycles K n
-- Init.Data.List.Lemmas
List.filter_sublist : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, (List.filter p l).Sublist l
-- Mathlib.Combinatorics.SimpleGraph.UniversalVerts
SimpleGraph.disjoint_image_val_universalVerts : ∀ {V : Type u_1} {G : SimpleGraph V} (s : Set ↑G.deleteUniversalVerts.verts),
  Disjoint (Subtype.val '' s) G.universalVerts
-- Init.Data.BitVec.Basic
BitVec.instAndOp : {w : ℕ} → AndOp (BitVec w)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.indep_singleton : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.Indep {e} ↔ M.IsNonloop e
-- Mathlib.CategoryTheory.EpiMono
/-- In a category in which every monomorphism is split, every monomorphism splits. This is not an
instance because it would create an instance loop.  -/
CategoryTheory.isSplitMono_of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.SplitMonoCategory C] {X Y : C} (f : Y ⟶ X)
  [CategoryTheory.Mono f], CategoryTheory.IsSplitMono f
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.smul_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {N : Type u_6}
  [inst_4 : TopologicalSpace N] [inst_5 : ChartedSpace H N] {E'' : Type u_7} [inst_6 : NormedAddCommGroup E'']
  [inst_7 : NormedSpace 𝕜 E''] {H'' : Type u_8} [inst_8 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''}
  {N' : Type u_9} [inst_9 : TopologicalSpace N'] [inst_10 : ChartedSpace H'' N'] {n : WithTop ℕ∞} {V : Type u_10}
  [inst_11 : NormedAddCommGroup V] [inst_12 : NormedSpace 𝕜 V] (r : 𝕜)
  (g : ContMDiffMap I'' (modelWithCornersSelf 𝕜 V) N' V n) (h : ContMDiffMap I I'' N N' n),
  (r • g).comp h = r • g.comp h
-- Lean.Meta.LitValues
/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt64` with value `n`.  -/
Lean.Meta.getUInt64Value? : Lean.Expr → Lean.MetaM (Option UInt64)
-- Lean.Meta.Tactic.Grind.PropagatorAttr
Lean.Meta.Grind.registerBuiltinDownwardPropagator : Lean.Name → Lean.Meta.Grind.Propagator → IO Unit
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.isoEquiv_symm_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (e : F.obj X ≅ F.obj Y),
  hF.isoEquiv.symm e = hF.preimageIso e
-- Mathlib.RingTheory.Discriminant
/-- If `b` is a basis of a finite separable field extension `L/K`,
then `Algebra.discr K b` is a unit.  -/
Algebra.discr_isUnit_of_basis : ∀ {ι : Type w} [inst : DecidableEq ι] [inst_1 : Fintype ι] (K : Type u) {L : Type v} [inst_2 : Field K]
  [inst_3 : Field L] [inst_4 : Algebra K L] [Module.Finite K L] [Algebra.IsSeparable K L] (b : Module.Basis ι K L),
  IsUnit (Algebra.discr K ⇑b)