mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order
continuous_bot : ∀ {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace β}, Continuous f
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.limitConstTerminal_inv_π : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasTerminal C] {j : J},
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.limitConstTerminal.inv
      (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.const J).obj (⊤_ C)) j) =
    CategoryTheory.Limits.terminal.from (⊤_ C)
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_bound' : ∀ {x : ℂ} {n : ℕ},
  ‖x‖ / ↑n.succ ≤ 1 / 2 → ‖Complex.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial‖ ≤ ‖x‖ ^ n / ↑n.factorial * 2
-- Init.Data.SInt.Bitwise
Int16.toISize_xor : ∀ (a b : Int16), (a ^^^ b).toISize = a.toISize ^^^ b.toISize
-- Mathlib.Data.FunLike.Group
FunLike.subNegZeroMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Zero F]
  [inst_3 : SMul ℕ F] [inst_4 : Neg F] [inst_5 : Sub F] [inst_6 : SMul ℤ F] [inst_7 : SubNegZeroMonoid β]
  [inst_8 : IsZeroApply F α β] [inst_9 : IsAddApply F α β] [inst_10 : IsNegApply F α β] [inst_11 : IsSubApply F α β]
  [inst_12 : IsSMulApply ℕ F α β] [inst_13 : IsSMulApply ℤ F α β],
  FunLike.subNegZeroMonoid = Function.Injective.subNegZeroMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.Multiset.AddSub
Multiset.rel_add_right : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {as : Multiset α} {bs₀ bs₁ : Multiset β},
  Multiset.Rel r as (bs₀ + bs₁) ↔ ∃ as₀ as₁, Multiset.Rel r as₀ bs₀ ∧ Multiset.Rel r as₁ bs₁ ∧ as = as₀ + as₁
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.nat_add_iff : ∀ {p x : ℝ} {n : ℕ}, LiouvilleWith p (↑n + x) ↔ LiouvilleWith p x
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- **Alias** of the forward direction of `AddAction.isBlock_iff_vadd_eq_of_nonempty`. -/
AddAction.IsBlock.vadd_eq_of_nonempty : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X},
  AddAction.IsBlock G B → ∀ ⦃g : G⦄, ((g +ᵥ B) ∩ B).Nonempty → g +ᵥ B = B
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNNNorm_mul : ∀ {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype l] [inst_1 : Fintype m]
  [inst_2 : Fintype n] [inst_3 : NonUnitalSeminormedRing α] (A : Matrix l m α) (B : Matrix m n α),
  ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
/-- **Alias** of `simplyConnectedSpace_iff`. -/
simply_connected_def : ∀ (X : Type u_3) [inst : TopologicalSpace X],
  SimplyConnectedSpace X ↔ Nonempty (FundamentalGroupoid X ≌ CategoryTheory.Discrete Unit)
-- Mathlib.Data.Finset.NAry
Finset.image₂_subset_iff : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
  {u : Finset γ}, Finset.image₂ f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.self_lt_rpow_of_lt_one : ∀ {x y : ℝ}, 0 < x → x < 1 → y < 1 → x < x ^ y
-- Lean.Meta.Tactic.Contradiction
_private.Lean.Meta.Tactic.Contradiction.0.Lean.Meta.elimEmptyInductive : Lean.MVarId → Lean.FVarId → ℕ → Lean.MetaM Bool
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.isIndContained_iff_exists_iso_induce : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W},
  G.IsIndContained H ↔ ∃ s, Nonempty (G ≃g SimpleGraph.induce s H)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lift_mul : ∀ (a b : Ordinal.{v}), Ordinal.lift.{u, v} (a * b) = Ordinal.lift.{u, v} a * Ordinal.lift.{u, v} b
-- Mathlib.Order.Filter.Pointwise
Filter.smul_pure : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter α} {b : β}, f • pure b = Filter.map (fun x => x • b) f
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerRight : Lean.Expr →
  Mathlib.Tactic.BicategoryLike.Mor₁ →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Init.Data.BitVec.Bootstrap
BitVec.getMsbD.eq_1 : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), x.getMsbD i = (decide (i < w) && x.getLsbD (w - 1 - i))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_eq_some_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.maxKey? = some (t.maxKey he)
-- Mathlib.MeasureTheory.Group.Arithmetic
List.measurable_fun_sum : ∀ {M : Type u_2} {α : Type u_3} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M]
  {m : MeasurableSpace α} (l : List (α → M)),
  (∀ f ∈ l, Measurable f) → Measurable fun x => (List.map (fun f => f x) l).sum
-- Init.Data.List.Sublist
List.IsSuffix.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁.Sublist l₂
-- Init.Data.SInt.Lemmas
ISize.toInt_lt : ∀ (x : ISize), x.toInt < 2 ^ 63
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.forget_obj : ∀ (R : Type u) [inst : CommRing R] {A : AlgCat R}, (CategoryTheory.forget (AlgCat R)).obj A = ↑A
-- Init.Data.Int.Order
Int.lt_add_of_pos_left : ∀ (a : ℤ) {b : ℤ}, 0 < b → a < b + a
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.instInhabitedSuggestion : Inhabited Lean.Meta.Tactic.TryThis.Suggestion
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instAddSemigroup : {R : Type u_3} → {A : Type u_4} → [AddSemigroup R] → [AddSemigroup A] → AddSemigroup (Unitization R A)
-- Mathlib.Order.UpperLower.Relative
IsUpperSet.isRelUpperSet_sep : ∀ {α : Type u_1} {s : Set α} (P : α → Prop) [inst : LE α], IsUpperSet s → IsRelUpperSet {x | x ∈ s ∧ P x} P
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_filter_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k k' : α} {fallback : β},
  (↑m).WF →
    m.getKey? k = some k' →
      Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.filter f m) k fallback =
        (Option.filter (fun x => f k' x) (Std.DHashMap.Internal.Raw₀.Const.get? m k)).getD fallback
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.space.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] (K : Geometry.SimplicialComplex 𝕜 E), K.space = ⋃ s ∈ K.faces, (convexHull 𝕜) ↑s
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
/-- Continuity of `(x, y) ↦ x ^ y` as a function on `ℝ × ℂ`.  -/
Complex.continuousAt_ofReal_cpow : ∀ (x : ℝ) (y : ℂ), 0 < y.re ∨ x ≠ 0 → ContinuousAt (fun p => ↑p.1 ^ p.2) (x, y)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.LocallyQuasiFinite.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.LocallyQuasiFinite (CategoryTheory.CategoryStruct.comp f g)],
  AlgebraicGeometry.LocallyQuasiFinite f
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.AffineOpenCover.openCover_f : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.AffineOpenCover) (j : 𝒰.I₀), 𝒰.openCover.f j = 𝒰.f j
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
/-- **Alias** of the forward direction of `MeasureTheory.memLp_piLp_iff`. -/
MeasureTheory.MemLp.eval_piLp : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {p q : ENNReal} [inst : Fact (1 ≤ q)]
  {ι : Type u_2} [inst_1 : Fintype ι] {E : ι → Type u_3} [inst_2 : (i : ι) → NormedAddCommGroup (E i)]
  {f : X → PiLp q E}, MeasureTheory.MemLp f p μ → ∀ (i : ι), MeasureTheory.MemLp (fun x => (f x).ofLp i) p μ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  {Y Z : C} (f : Y ⟶ Z) {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X Z) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) h
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.insertMany : {α : Type u_1} →
  [inst : BEq α] →
    [inst_1 : Hashable α] → {ρ : Type u_2} → [ForIn Id ρ α] → ρ → Aesop.OrderedHashSet α → Aesop.OrderedHashSet α
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.toWithBotSyn_apply_le_bot_iff : ∀ {σ : Type u_1} (m : MonomialOrder σ) (a : WithBot (σ →₀ ℕ)), m.toWithBotSyn a ≤ ⊥ ↔ a = ⊥
-- Lean.Parser.Syntax
Lean.Parser.Command.prefix.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instOrdOrdinal : Ord Std.Time.Millisecond.Ordinal
-- Std.Internal.Parsec.ByteArray
/-- Parse a `Char` that can be represented in 1 byte. If `c` uses more than 1 byte it is truncated.
 -/
Std.Internal.Parsec.ByteArray.pByteChar : Char → Std.Internal.Parsec.ByteArray.Parser Char
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomInvPair.ids : ∀ {R₁ : Type u_1} [inst : Semiring R₁], RingHomInvPair (RingHom.id R₁) (RingHom.id R₁)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_neg : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup F] (f : α → F) (q : ℝ)
  (μ : MeasureTheory.Measure α), MeasureTheory.eLpNorm' (-f) q μ = MeasureTheory.eLpNorm' f q μ
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.ematchTheorem : Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.EMatch.M Unit
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.refl_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.Iso.refl X).symm = CategoryTheory.Iso.refl X
-- Init.Coe
instCoeTOfCoeDep : {α : Sort u_1} → {a : α} → {β : Sort u_2} → [CoeDep α a β] → CoeT α a β
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sumAddHom.eq_1 : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ),
  DFinsupp.sumAddHom φ = { toZeroHom := DFinsupp.sumZeroHom fun i => ↑(φ i), map_add' := ⋯ }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.union!_insert_right_equiv_insert_union! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  {p : (a : α) × β a},
  m₁.WF →
    m₂.WF →
      (m₁.union! (Std.DTreeMap.Internal.Impl.insert! p.fst p.snd m₂)).Equiv
        (Std.DTreeMap.Internal.Impl.insert! p.fst p.snd (m₁.union! m₂))
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.DefaultConsumers.forIn'_eq_wf_of_finite : ∀ {m : Type w → Type w'} {α β : Type w} [inst : Std.Iterator α m β] [inst_1 : Std.Iterators.Finite α m]
  {n : Type x → Type x'} [inst_2 : Monad n] [LawfulMonad n] {lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ}
  {γ : Type x} {it : Std.IterM m β} {init : γ} {P : β → Prop} {hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b}
  (f : (b : β) → P b → γ → n { x // True }),
  Std.IterM.DefaultConsumers.forIn' lift γ (fun x x_1 x_2 => True) it init P hP f =
    Std.IterM.DefaultConsumers.forIn'.wf lift γ (fun x x_1 x_2 => True) ⋯ it init P hP f
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.instInhabitedGeneralTheorem : Inhabited Mathlib.Meta.FunProp.GeneralTheorem
-- Lean.Data.Json.Basic
Lean.JsonNumber.instOrd : Ord Lean.JsonNumber
-- Init.System.Promise
/-- Like `Promise.result`, but resolves to `none` if the promise is dropped without ever being resolved.
 -/
IO.Promise.result? : {α : Type} → IO.Promise α → Task (Option α)
-- Lean.LabelAttribute
/-- Initialize a new "label" attribute.
Declarations tagged with the attribute can be retrieved using `Lean.labelled`.
 -/
Lean.Parser.Command.registerLabelAttr : Lean.ParserDescr
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Relation.mk'_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {fst snd : S.Arrow} (r : fst.Relation snd),
  (CategoryTheory.GrothendieckTopology.Cover.Relation.mk' r).fst = fst
-- Mathlib.Topology.ClopenBox
TopologicalSpace.Clopens.countable_iff_secondCountable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X],
  Countable (TopologicalSpace.Clopens X) ↔ SecondCountableTopology X
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
LinearMap.BilinForm.tensorDistribEquiv_tmul : ∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] [inst_5 : Module.Free R M₁]
  [inst_6 : Module.Finite R M₁] [inst_7 : Module.Free R M₂] [inst_8 : Module.Finite R M₂]
  (B₁ : LinearMap.BilinForm R M₁) (B₂ : LinearMap.BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂),
  (((LinearMap.BilinForm.tensorDistribEquiv R) (B₁ ⊗ₜ[R] B₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂') = (B₁ m₁) m₁' * (B₂ m₂) m₂'
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.AppImplicitArg.optional.inj : ∀ {name : Lean.Name} {s : Lean.Term} {name_1 : Lean.Name} {s_1 : Lean.Term},
  Lean.PrettyPrinter.Delaborator.AppImplicitArg.optional name s =
      Lean.PrettyPrinter.Delaborator.AppImplicitArg.optional name_1 s_1 →
    name = name_1 ∧ s = s_1
-- Mathlib.Order.Partition.Basic
/-- A predicate characterizing when a function `f : α → α` is a representative function for a
partition `P`. A representative function maps each element to a canonical representative in its
equivalence class, is the identity outside the support, and maps related elements to the same
representative.  -/
Partition.IsRepFun : {α : Type u_1} → {u : Set α} → Partition u → (α → α) → Prop
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.closureAddCommGroupOfComm.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x + y = y + x),
  AddSubgroup.closureAddCommGroupOfComm hcomm = inferInstance
-- Std.Internal.Do.Order.Basic
/-- Binary join (supremum)  -/
Lean.Order.«term_⊔_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.mapEquiv_refl : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  DividedPowerAlgebra.mapEquiv (LinearEquiv.refl R M) = AlgEquiv.refl
-- Lean.Parser.Extension
Lean.Parser.evalParserConst : Lean.Name → optParam (Option Lean.Parser.ParserFn) none → Lean.Parser.ParserFn
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    ⟨k, v⟩ ∈ l → (Std.ExtDHashMap.ofList l).getD k' fallback = cast ⋯ v
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of an n-ary product is the sup of the nilpotency classes of
the factors.  -/
AddGroup.nilpotencyClass_pi : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → AddGroup (Gs i)] [inst_1 : Fintype η]
  [∀ (i : η), AddGroup.IsNilpotent (Gs i)],
  AddGroup.nilpotencyClass ((i : η) → Gs i) = Finset.univ.sup fun i => AddGroup.nilpotencyClass (Gs i)
-- Init.Data.Ord.Basic
/-- Greater than.  -/
Ordering.gt : Ordering
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- A linear isometric equivalence preserves the property of being orthonormal.  -/
Orthonormal.comp_linearIsometryEquiv : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] {v : ι → E},
  Orthonormal 𝕜 v → ∀ (f : E ≃ₗᵢ[𝕜] E'), Orthonormal 𝕜 (⇑f ∘ v)
-- Mathlib.Analysis.CStarAlgebra.Spectrum
WeakDual.CharacterSpace.instStarHomClass : ∀ {A : Type u_2} [inst : CStarAlgebra A], StarHomClass (↑(WeakDual.characterSpace ℂ A)) A ℂ
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithTerminal.map.match_1.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3) (a : C)
  (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star)
  (h_1 :
    (a a_1 : C) →
      (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1) →
        motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_1) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => h_1 a a_1 f
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => h_2 a x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_2 a x
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.rel_iff : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (x y : R), I.ringCon x y ↔ x - y ∈ I
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_not_succ_of_ne_bsup : ∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}},
  (∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ o.bsup f) → ∀ a < o.bsup f, Order.succ a < o.bsup f
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.denote.eq_7 : ∀ (ctx : Int.Internal.Linear.Context) (e : Int.Internal.Linear.Expr) (k : ℤ),
  Int.Internal.Linear.Expr.denote ctx (e.mulR k) = Int.Internal.Linear.Expr.denote ctx e * k
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instAddZeroClass : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → [AddZeroClass A] → AddZeroClass (CStarMatrix m n A)
-- Std.Time.Date.Unit.Month
Std.Time.Month.instLEOrdinal : LE Std.Time.Month.Ordinal
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderivWithin_sub : ∀ {𝕜 : 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_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {s : Set M} {g g' : M → F} {x : M},
  MDiffAt[s] g x → MDiffAt[s] g' x → UniqueMDiffAt[s] x → d[s] (g - g') x = d[s] g x - d[s] g' x
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_pos : ∀ (o : Ordinal.{u_1}), 0 < Cardinal.beth o
-- Mathlib.Algebra.Order.Star.Basic
IsSelfAdjoint.mul_self_nonneg : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {a : R}, IsSelfAdjoint a → 0 ≤ a * a
-- Mathlib.Order.Filter.Basic
Filter.eventually_imp_distrib_left : ∀ {α : Type u} {f : Filter α} {p : Prop} {q : α → Prop}, (∀ᶠ (x : α) in f, p → q x) ↔ p → ∀ᶠ (x : α) in f, q x
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.eventuallyEq_one : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X) (hx : x ∈ s),
  ⇑(f (f.ind x hx)) =ᶠ[nhds x] 1
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.Limits.coneOfSectionCompCoyoneda_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) (s : ↑(F.comp (CategoryTheory.coyoneda.obj X)).sections),
  (CategoryTheory.Limits.coneOfSectionCompCoyoneda F X s).pt = Opposite.unop X
-- Init.Control.Lawful.Basic
/-- This is just a duplicate of `LawfulApplicative.map_pure`,
but sometimes applies when that doesn't.

It is named with a prime to avoid conflict with the inherited field `LawfulMonad.map_pure`.
 -/
LawfulMonad.map_pure' : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} {f : α → β} [inst : Monad m] [LawfulMonad m] {a : α},
  f <$> pure a = pure (f a)
-- Mathlib.FieldTheory.IntermediateField.Algebraic
IntermediateField.finrank_lt_of_gt : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  [FiniteDimensional (↥F) L], F < E → Module.finrank (↥E) L < Module.finrank (↥F) L
-- Init.Data.Order.Lemmas
Std.instMinEqOrOfLawfulOrderLeftLeaningMin : ∀ {α : Type u} [inst : LE α] [inst_1 : Min α] [Std.LawfulOrderLeftLeaningMin α], Std.MinEqOr α
-- Mathlib.Tactic.Push.Attr
Mathlib.Tactic.Push.Head.forall.sizeOf_spec : sizeOf Mathlib.Tactic.Push.Head.forall = 1
-- Mathlib.Data.Seq.Computation
Computation.mem_unique : ∀ {α : Type u} {s : Computation α} {a b : α}, a ∈ s → b ∈ s → a = b
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.Hom.toCoalgHom_injective : ∀ {R : Type u} [inst : CommRing R] (V W : CoalgCat R), Function.Injective CoalgCat.Hom.toCoalgHom'
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- If `E` is a normed space, `Lp.simpleFunc E p μ` is a module. Not declared as an
instance as it is (as of writing) used only in the construction of the Bochner integral.  -/
MeasureTheory.Lp.simpleFunc.module : {α : Type u_1} →
  {E : Type u_4} →
    {𝕜 : Type u_6} →
      [inst : MeasurableSpace α] →
        [inst_1 : NormedAddCommGroup E] →
          {p : ENNReal} →
            {μ : MeasureTheory.Measure α} →
              [inst_2 : NormedRing 𝕜] →
                [inst_3 : Module 𝕜 E] → [IsBoundedSMul 𝕜 E] → Module 𝕜 ↥(MeasureTheory.Lp.simpleFunc E p μ)
-- Init.Control.EState
EStateM.instMonadFinally : {ε σ : Type u} → MonadFinally (EStateM ε σ)
-- Mathlib.CategoryTheory.Sites.CoverLifting
/-- Auxiliary definition for `isLimitMultifork`  -/
CategoryTheory.RanIsSheafOfIsCocontinuous.lift : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {G : CategoryTheory.Functor C D} →
          {A : Type w} →
            [inst_2 : CategoryTheory.Category.{w', w} A] →
              {J : CategoryTheory.GrothendieckTopology C} →
                {K : CategoryTheory.GrothendieckTopology D} →
                  [G.IsCocontinuous J K] →
                    {F : CategoryTheory.Functor Cᵒᵖ A} →
                      CategoryTheory.Presheaf.IsSheaf J F →
                        {R : CategoryTheory.Functor Dᵒᵖ A} →
                          {α : G.op.comp R ⟶ F} →
                            (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension →
                              {X : D} →
                                {S : K.Cover X} →
                                  (s : CategoryTheory.Limits.Multifork (S.index R)) → s.pt ⟶ R.obj (Opposite.op X)
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.logEmbedding.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.Units.logEmbedding K =
    {
      toFun := fun x w =>
        ↑(↑w).mult * Real.log (↑w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(Additive.toMul x))),
      map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Group.AddChar
AddChar.zero_apply : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (a : A), 0 a = 1
-- Mathlib.Topology.UniformSpace.Basic
Uniform.continuousOn_iff'_right : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : TopologicalSpace β] {f : β → α} {s : Set β},
  ContinuousOn f s ↔ ∀ b ∈ s, Filter.Tendsto (fun x => (f b, f x)) (nhdsWithin b s) (uniformity α)
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
not_isStationary_iff : ∀ {α : Type v} {s : Set α} [inst : LinearOrder α], ¬IsStationary s ↔ ∃ t, IsClub t ∧ Disjoint s t