mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Function.Defs
/-- Composition of dependent functions: `(f ∘' g) x = f (g x)`, where type of `g x` depends on `x`
and type of `f (g x)` depends on `x` and `g x`.  -/
Function.dcomp : {α : Sort u₁} →
  {β : α → Sort u₂} →
    {φ : {x : α} → β x → Sort u₃} → ({x : α} → (y : β x) → φ y) → (g : (x : α) → β x) → (x : α) → φ (g x)
-- Mathlib.Order.Cover
/-- **Alias** of the forward direction of `covBy_iff_lt_iff_le_left`. -/
CovBy.lt_iff_le_left : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α}, x ⋖ y → ∀ {z : α}, z < y ↔ z ≤ x
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
arithGeom_same_eq_sum : ∀ {R : Type u_1} {a b : R} [inst : CommSemiring R] (n : ℕ), arithGeom a b b n = b * ∑ k ∈ Finset.range (n + 1), a ^ k
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Functor.OplaxMonoidal.whiskeringRight_η_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory D] [inst_4 : CategoryTheory.MonoidalCategory E]
  (L : CategoryTheory.Functor D E) [inst_5 : L.OplaxMonoidal] (X : C),
  (CategoryTheory.Functor.OplaxMonoidal.η ((CategoryTheory.Functor.whiskeringRight C D E).obj L)).app X =
    CategoryTheory.Functor.OplaxMonoidal.η L
-- Init.Data.UInt.Basic
/-- Subtracts one 8-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the `-` operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.sub : UInt8 → UInt8 → UInt8
-- Mathlib.RingTheory.AdicCompletion.Exactness
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapExactAux.eq_def : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {M : Type u} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : Type u} [inst_5 : AddCommGroup P]
  [inst_6 : Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g)
  (hg : Function.Surjective ⇑g) {k : ℕ} (hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range))
  (x : AdicCompletion.AdicCauchySequence I N) (hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤) (x_1 : ℕ),
  AdicCompletion.mapExactAux✝ hf hfg hg hkn x hker x_1 =
    match x_1 with
    | Nat.zero =>
      let d := ⋯.choose;
      let y := ⋯.choose;
      have hdy := ⋯;
      have hdmem := ⋯;
      ⟨y, ⋯⟩
    | n.succ =>
      let d := ⋯.choose;
      let y := ⋯.choose;
      have hdy := ⋯;
      have hdmem := ⋯;
      match AdicCompletion.mapExactAux✝ hf hfg hg hkn x hker n with
      | ⟨yₙ, hyₙ⟩ =>
        match AdicCompletion.mapExactAuxDelta✝ hf hkn x hdmem hdy hyₙ with
        | ⟨d, hd⟩ => ⟨yₙ + ↑d, hd⟩
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_monadMap_ReaderT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ρ : Type u}
  (f : {β : Type u} → m β → m β) {α : Type u} (x : ReaderT ρ m α) (post : α → ρ → Pred) (epost : EPred),
  Std.Internal.Do.wp (MonadFunctor.monadMap (fun {β} => f) x) post epost = fun r =>
    Std.Internal.Do.wp (f (x.run r)) (fun a => post a r) epost
-- Mathlib.Data.ENNReal.BigOperators
/-- seeing `ℝ≥0∞` as `Real` does not change their sum, unless one of the `ℝ≥0∞` is infinity  -/
ENNReal.toReal_sum : ∀ {α : Type u_1} {s : Finset α} {f : α → ENNReal}, (∀ a ∈ s, f a ≠ ⊤) → (∑ a ∈ s, f a).toReal = ∑ a ∈ s, (f a).toReal
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.inv_mem_transvections_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {e : V ≃ₗ[R] V},
  e⁻¹ ∈ LinearEquiv.transvections R V ↔ e ∈ LinearEquiv.transvections R V
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k : α} {f : Option β → Option β} {hc : k ∈ Std.DTreeMap.Raw.Const.alter t k f},
  Std.DTreeMap.Raw.Const.get (Std.DTreeMap.Raw.Const.alter t k f) k hc = (f (Std.DTreeMap.Raw.Const.get? t k)).get ⋯
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.isCaratheodory_iff_le' : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α},
  m.IsCaratheodory s ↔ ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.colimitCocone_isColimit_desc : ∀ {α : Type u} [inst : CompleteLattice α] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J α) (s : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.CompleteLattice.colimitCocone F).isColimit.desc s = CategoryTheory.homOfLE ⋯
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.mem_range_lift_of_card_le : ∀ {a : Cardinal.{u}} {b : Ordinal.{max u v}}, b.card ≤ Cardinal.lift.{v, u} a → b ∈ Set.range Ordinal.lift.{v, u}
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- A version of `Matrix.invertibleOfDetInvertible` with the inverse defeq to `A⁻¹` that is
therefore noncomputable.  -/
Matrix.invertibleOfIsUnitDet : {n : Type u'} →
  {α : Type v} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] → [inst_2 : CommRing α] → (A : Matrix n n α) → IsUnit A.det → Invertible A
-- Aesop.Index.Basic
/-- The source of a rule match reported by the index. We assume that
only IndexMatchLocations belonging to the same goal are equated or compared.  -/
Aesop.IndexMatchLocation : Type
-- Mathlib.Analysis.Normed.Group.Basic
smul_ball'' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a b : E} {r : ℝ}, a • Metric.ball b r = Metric.ball (a • b) r
-- Init.Data.Nat.MinMax
Nat.mul_min_mul_right : ∀ (a b c : ℕ), min (a * c) (b * c) = min a b * c
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENatAux_eq_nat : ∀ {x : Cardinal.{u_1}} {n : ℕ}, x.toENatAux = ↑n ↔ x = ↑n
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the coherence composition `η ⊗≫ θ := η ≫ α ≫ θ`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂.coherenceCompM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂ m] →
    Mathlib.Tactic.BicategoryLike.CoherenceHom →
      Mathlib.Tactic.BicategoryLike.Mor₂ → Mathlib.Tactic.BicategoryLike.Mor₂ → m Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Multiplicativity of a multilinear map along all coordinates at the same time,
writing `f (fun i => c i • m i)` as `(∏ i, c i) • f m`.  -/
MultilinearMap.map_smul_univ : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : Fintype ι] (c : ι → R) (m : (i : ι) → M₁ i),
  (f fun i => c i • m i) = (∏ i, c i) • f m
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.mem_support_C_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] {n a : ℕ} {c : R}, a ∈ (Polynomial.C c * Polynomial.X ^ n).support → a = n
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- The carrier of `N ⊔ H` is just `↑N + ↑H` (pointwise set addition)
when `N` is normal.  -/
AddSubgroup.normal_add : ∀ {G : Type u_2} [inst : AddGroup G] (N H : AddSubgroup G) [N.Normal], ↑(N ⊔ H) = ↑N + ↑H
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.ext_iff : ∀ {G : Type u} {inst : Group G} {inst_1 : TopologicalSpace G} {x y : OpenNormalSubgroup G},
  x = y ↔ (↑x.toOpenSubgroup).carrier = (↑y.toOpenSubgroup).carrier
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.coeffs.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e e_1 : ι → M} (e_e : e = e_1) {ε ε_1 : ι → Module.Dual R M} (e_ε : ε = ε_1) (h : Module.DualBases e ε) (m m_1 : M),
  m = m_1 → h.coeffs m = ⋯.coeffs m_1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceIsLower : Lean.Meta.Simp.DSimproc
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryLT_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {h' : ∃ a ∈ t₁, cmp a k = Ordering.lt} (h : t₁.Equiv t₂),
  Std.DTreeMap.Const.getEntryLT t₁ k h' = Std.DTreeMap.Const.getEntryLT t₂ k ⋯
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.comm₁_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]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃) {Z : C} (h : X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.m₁ (CategoryTheory.CategoryStruct.comp v₁₃ h) =
    CategoryTheory.CategoryStruct.comp v₁₂ h
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.coe_map : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (S : AddSubsemigroup M),
  ↑(AddSubsemigroup.map f S) = ⇑f '' ↑S
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  k ∈ t.insertMany l ↔ k ∈ t ∨ (List.map Prod.fst l).contains k = true
-- Mathlib.Algebra.Ring.BooleanRing
instInhabitedAsBoolAlg : {α : Type u_1} → [Inhabited α] → Inhabited (AsBoolAlg α)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiff_nat_iff_continuous_differentiable : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : ℕ},
  ContDiff 𝕜 (↑n) f ↔
    (∀ m ≤ n, Continuous fun x => iteratedFDeriv 𝕜 m f x) ∧ ∀ m < n, Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
/-- A simplicial set `X` is a Kan complex iff for any `n : ℕ`, `i : Fin (n + 2)`,
and any family of morphisms `Δ[n] ⟶ Z` for all `j ≠ i` that is compatible
(in the sense that it extends to a morphism `Λ[n + 1, i] ⟶ X`), there
exists a morphism `Δ[n + 1] ⟶ Z` which induces the given family of morphisms
on the faces `j ≠ i`.  -/
SSet.KanComplex.iff : ∀ {Z : SSet},
  Z.KanComplex ↔
    ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ Z)),
      SSet.horn.IsCompatible f →
        ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) φ = f j hj
-- Std.Data.Iterators.Lemmas.Combinators.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Drop.0.Std.IterM.step_drop.match_3.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.instDeterministicHomBraiding : ∀ {X Y : SFinKer}, CategoryTheory.Deterministic (β_ X Y).hom
-- Mathlib.Topology.Homotopy.Lifting
IsAddQuotientCoveringMap.ker_fundamentalGroupToMulOpposite : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hp : IsAddQuotientCoveringMap p G) {x : X} (e : ↑(p ⁻¹' {x})),
  (hp.fundamentalGroupToMulOpposite e).ker = (⋯.monodromyPerm x).ker
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.toWithBotNat.congr_simp : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (x x_1 : R),
  x = x_1 → IsDiscreteValuationRing.toWithBotNat x = IsDiscreteValuationRing.toWithBotNat x_1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_insert_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (h : m.WF) {k : α} {v : β k}, (m.insert k v).get k ⋯ = v
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.instOrderTop : {α : Type u_2} → [inst : TopologicalSpace α] → {x : α} → OrderTop (TopologicalSpace.OpenNhdsOf x)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.completeBasis.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.completeBasis K =
    NumberField.mixedEmbedding.fundamentalCone.completeBasis K
-- Mathlib.Data.Nat.Multiplicity
Nat.emultiplicity_two_factorial_lt : ∀ {n : ℕ}, n ≠ 0 → emultiplicity 2 n.factorial < ↑n
-- Mathlib.Topology.Algebra.Order.Floor
/-- Do not use this, use `ContinuousOn.comp_fract` instead.  -/
ContinuousOn.comp_fract' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α]
  [inst_3 : TopologicalSpace α] [IsStrictOrderedRing α] [OrderTopology α] [inst_6 : TopologicalSpace β]
  [inst_7 : TopologicalSpace γ] {f : β → α → γ},
  ContinuousOn (Function.uncurry f) (Set.univ ×ˢ Set.Icc 0 1) →
    (∀ (s : β), f s 0 = f s 1) → Continuous fun st => f st.1 (Int.fract st.2)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- A `Sphere P` bundles a `center` and `radius`. This definition does not require the radius to
be positive; that should be given as a hypothesis to lemmas that require it.  -/
EuclideanGeometry.Sphere : (P : Type u_2) → [MetricSpace P] → Type u_2
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi.isAddLeftInvariant : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → AddGroup (α i)] [∀ (i : ι), MeasurableAdd (α i)] [∀ (i : ι), (μ i).IsAddLeftInvariant],
  (MeasureTheory.Measure.pi μ).IsAddLeftInvariant
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharThreeNF_spec : ∀ {F : Type u_2} [inst : Field F] [inst_1 : CharP F 3] (W : WeierstrassCurve F), (W.toCharThreeNF • W).IsCharThreeNF
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.BifibrantObject.instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.BifibrantObject C),
  HomotopicalAlgebra.IsFibrant (HomotopicalAlgebra.BifibrantObject.ιCofibrantObject.obj X).obj
-- Mathlib.Data.Finite.Defs
instFinitePLift : ∀ {α : Sort u_1} [Finite α], Finite (PLift α)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.instT0Space : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  T0Space (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property `P` of ring homs satisfies `RingHom.StableUnderCompositionWithLocalizationAwaySource`
if whenever `P` holds for `f` it also holds for the composition with
localization maps on the source.  -/
RingHom.StableUnderCompositionWithLocalizationAwaySource : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Finite
/-- **Alias** of the reverse direction of `Set.infinite_smul_set`. -/
Set.Infinite.smul_set : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a : G} {s : Set α},
  s.Infinite → (a • s).Infinite
-- Init.Data.Array.Zip
_private.Init.Data.Array.Zip.0.List.getElem?_zipWithAll.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (h_1 : Unit → motive none none)
  (h_2 : (a? : Option α) → (b? : Option β) → motive a? b?),
  (match none, none with
    | none, none => h_1 ()
    | a?, b? => h_2 a? b?) =
    h_1 ()
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_neg : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : ContinuousNeg M], ⇑(ContinuousLinearEquiv.neg R) = -id
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.toMulHom_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N] (f : M →* N), (↑f).toFun = ⇑f
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.below.left : ∀ {motive : (a : ℕ → ℕ) → Nat.Primrec a → Prop}, Nat.Primrec.below Nat.Primrec.left
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet_id : ∀ {𝕜 : Type u_1} {U : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U] [inst_2 : InnerProductSpace 𝕜 U]
  [inst_3 : FiniteDimensional 𝕜 U], LinearMap.id.normDet = 1
-- Batteries.Lean.PersistentHashMap
/-- Variant of `ofList` which accepts a function that combines values of duplicated
keys.
 -/
Lean.PersistentHashMap.ofListWith : {α : Type u_1} →
  [inst : BEq α] → [inst_1 : Hashable α] → {β : Type u_2} → List (α × β) → (α → β → β → β) → Lean.PersistentHashMap α β
-- Batteries.Data.Fin.Coding
Fin.encodeChar_decodeChar : ∀ (x : Fin Char.count), Fin.encodeChar (Fin.decodeChar x) = x
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- The chosen coend construction as a functor out of the bifunctor category.  -/
CategoryTheory.Limits.chosenCoendFunctor : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} J] →
        [CategoryTheory.Limits.ChosenCoendsOfShape J C] →
          CategoryTheory.Functor (CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) C
-- Std.Sync.Broadcast
/-- Circular buffer storing broadcast messages accessible to all receivers.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.State.buffer : {α : Type} → (self : Std.Bounded.State✝ α) → Vector (IO.Ref (Std.Slot✝ α)) ↑(Std.Bounded.State.capacity✝ self)
-- Std.Data.DHashMap.Internal.AssocList.Basic
Std.DHashMap.Internal.AssocList.brecOn.eq : ∀ {α : Type u} {β : α → Type v} {motive : Std.DHashMap.Internal.AssocList α β → Sort u_1}
  (t : Std.DHashMap.Internal.AssocList α β)
  (F_1 : (t : Std.DHashMap.Internal.AssocList α β) → Std.DHashMap.Internal.AssocList.below t → motive t),
  Std.DHashMap.Internal.AssocList.brecOn t F_1 = F_1 t (Std.DHashMap.Internal.AssocList.brecOn.go t F_1).2
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.isClosed_cellFrontier`. -/
Topology.CWComplex.isClosed_cellFrontier : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] [T2Space X] {n : ℕ}
  {i : Topology.RelCWComplex.cell C n}, IsClosed (Topology.RelCWComplex.cellFrontier n i)
-- Aesop.Tree.Tracing
_private.Aesop.Tree.Tracing.0.Aesop.Rapp.traceMetadata.trc : Aesop.TraceOption → Lean.MessageData → Lean.MetaM Unit
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpInd_disjoint_union : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s t : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasurableSet s →
    MeasurableSet t →
      μ s ≠ ⊤ →
        μ t ≠ ⊤ →
          Disjoint s t →
            MeasureTheory.condExpInd G hm μ (s ∪ t) =
              MeasureTheory.condExpInd G hm μ s + MeasureTheory.condExpInd G hm μ t
-- Mathlib.Analysis.Calculus.FDeriv.Congr
differentiableWithinAt_congr_set : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s t : Set E},
  s =ᶠ[nhds x] t → (DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x)
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.eccent_le_one_iff : ∀ {α : Type u_1} {G : SimpleGraph α} (u : α), G.eccent u ≤ 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_iUnion_of_directed : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_4} [Countable ι] (f : α → ENNReal)
  {s : ι → Set α}, Directed (fun x1 x2 => x1 ⊆ x2) s → ∫⁻ (x : α) in ⋃ i, s i, f x ∂μ = ⨆ i, ∫⁻ (x : α) in s i, f x ∂μ
-- Aesop.Forward.State
/-- The pattern substitution came from the given hypothesis.  -/
Aesop.PatSubstSource.hyp : Lean.FVarId → Aesop.PatSubstSource
-- Mathlib.Order.TypeTags
WithTop.recTopCoe_top : ∀ {α : Type u_1} {C : WithTop α → Sort u_2} (d : C ⊤) (f : (a : α) → C ↑a), WithTop.recTopCoe d f ⊤ = d
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier`.

---

Version of `skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier` using `skeleton`.  -/
Topology.CWComplex.skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] {n : ℕ∞}
  {m : ℕ} {j : Topology.RelCWComplex.cell C m},
  n < ↑m →
    ↑(Topology.RelCWComplex.skeleton C n) ∩ Topology.RelCWComplex.closedCell m j =
      ↑(Topology.RelCWComplex.skeleton C n) ∩ Topology.RelCWComplex.cellFrontier m j
-- Mathlib.RingTheory.LinearDisjoint
/-- Linear disjointness is symmetric in a commutative ring.  -/
Subalgebra.LinearDisjoint.symm : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S}, A.LinearDisjoint B → B.LinearDisjoint A
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq : ∀ {M : Type u_1} [inst : MonoidWithZero M] [IsLeftCancelMulZero M] {e₁ e₂ f₁ f₂ L : M},
  e₁ = L * f₁ → e₂ = L * f₂ → L ≠ 0 → (e₁ = e₂) = (f₁ = f₂)
-- Batteries.Data.ByteArray
/-- `map f a` applies the function `f` to each element of the array.  -/
ByteArray.map : ByteArray → (UInt8 → UInt8) → ByteArray
-- Mathlib.MeasureTheory.Measure.RegularityCompacts
MeasureTheory.innerRegularWRT_isCompact_closure : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [SecondCountableTopology α]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [OpensMeasurableSpace α] (P : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure P], P.InnerRegularWRT (IsCompact ∘ closure) IsClosed