mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
_private.Mathlib.CategoryTheory.Limits.Shapes.Kernels.0.CategoryTheory.Limits.compNatIso.match_1.eq_2 : ∀ (motive : CategoryTheory.Limits.WalkingParallelPair → Sort u_1)
  (h_1 : Unit → motive CategoryTheory.Limits.WalkingParallelPair.zero)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingParallelPair.one),
  (match CategoryTheory.Limits.WalkingParallelPair.one with
    | CategoryTheory.Limits.WalkingParallelPair.zero => h_1 ()
    | CategoryTheory.Limits.WalkingParallelPair.one => h_2 ()) =
    h_2 ()
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.sSup_adj : ∀ {V : Type u} {s : Set (SimpleGraph V)} {a b : V}, (sSup s).Adj a b ↔ ∃ G ∈ s, G.Adj a b
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.comp_mono : ∀ {E : Type u_3} {F : Type u_4} [inst : AddGroup E] [inst_1 : AddGroup F] {p q : AddGroupSeminorm E} (f : F →+ E),
  p ≤ q → p.comp f ≤ q.comp f
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_tryCatch_MonadExcept_apply_eq : ∀ {Pred : Type u_2} {EPred : Type u_3} {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_1} {α : Type u}
  {post : α → Pred} {epost : EPred} [inst_4 : MonadExceptOf ε m] (x : m α) (h : ε → m α),
  Std.Internal.Do.wp (tryCatch x h) post epost = Std.Internal.Do.wp (MonadExceptOf.tryCatch x h) post epost
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.Parallel.direction_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ : AffineSubspace k P}, s₁.Parallel s₂ → s₁.direction = s₂.direction
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.GenPatternInfo.assign? : Lean.Meta.Grind.GenPatternInfo →
  Lean.Meta.Grind.EMatch.Choice → Lean.Expr → OptionT Lean.Meta.Grind.GoalM Lean.Meta.Grind.EMatch.Choice
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.liftAddGroupHom_apply : ∀ {α : Type u_2} (β : Type u_3) [inst : AddCommGroup β] (a : FreeAbelianGroup α) (f : α → β),
  (FreeAbelianGroup.liftAddGroupHom β a) f = (FreeAbelianGroup.lift f) a
-- Mathlib.Order.Basic
/-- **Alias** of `Decidable.eq_or_lt_of_le'`. -/
LE.le.eq_or_lt_dec' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α} [DecidableLE α], b ≤ a → a = b ∨ b < a
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- **Alias** of `Localization.AtPrime.algebraOfLiesOver`.

---

If `P` lies over `p`, then `Localization.AtPrime P` is an algebra over `Localization.AtPrime p`.
This is not an instance for performance reasons and to avoid diamonds in the situation where the top
ring is already an algebra over `Localization.AtPrime p` (e.g., this happens for `Ideal.Fiber`).  -/
Localization.AtPrime.instAlgebraOfLiesOver : {A : Type u_4} →
  {B : Type u_5} →
    [inst : CommSemiring A] →
      [inst_1 : CommSemiring B] →
        [inst_2 : Algebra A B] →
          (p : Ideal A) →
            [inst_3 : p.IsPrime] →
              (P : Ideal B) →
                [inst_4 : P.IsPrime] → [P.LiesOver p] → Algebra (Localization.AtPrime p) (Localization.AtPrime P)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ihom_coev_app_hom : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A B : Rep.{u, u, v} k G),
  (Rep.Hom.hom ((CategoryTheory.ihom.coev A).app B)).toLinearMap =
    (TensorProduct.mk k ↑A ↑((CategoryTheory.Functor.id (Rep.{u, u, v} k G)).obj B)).flip
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k k' : α},
      (k == k') = true →
        ∀ {h' : k' ∈ Std.DHashMap.Raw.Const.insertManyIfNewUnit m l},
          k ∉ m →
            List.Pairwise (fun a b => (a == b) = false) l →
              k ∈ l → (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).getKey k' h' = k
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.coe_toLinearMap_one : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], ↑1 = LinearMap.id
-- Lean.Compiler.CSimpAttr
_private.Lean.Compiler.CSimpAttr.0.Lean.Compiler.CSimp.isConstantReplacement? : Lean.Name → Lean.CoreM (Option Lean.Compiler.CSimp.Entry)
-- Mathlib.Topology.UniformSpace.Ultra.Basic
/-- A uniform space is ultrametric if the uniformity `𝓤 X` has a basis of equivalence relations.  -/
IsUltraUniformity : (X : Type u_1) → [UniformSpace X] → Prop
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
HasProd.sigma : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousMul α] [RegularSpace α]
  {γ : β → Type u_4} {f : (b : β) × γ b → α} {g : β → α} {a : α},
  HasProd f a → (∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)) → HasProd g a
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.VAddInvariantMeasure.add : ∀ {M : Type v} {α : Type w} [inst : VAdd M α] {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}
  [MeasureTheory.VAddInvariantMeasure M α μ] [MeasureTheory.VAddInvariantMeasure M α ν],
  MeasureTheory.VAddInvariantMeasure M α (μ + ν)
-- Lean.Data.Lsp.LanguageFeatures
/-- Position of the completion info that this completion item was created from.  -/
Lean.Lsp.ResolvableCompletionItemData.cPos? : Lean.Lsp.ResolvableCompletionItemData → Option ℕ
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (H : CategoryTheory.Functor C D)
  (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C) (X : (SimplexCategory.Truncated n)ᵒᵖ),
  (((CategoryTheory.SimplicialObject.Truncated.whiskering C D).obj H).obj F).obj X = H.obj (F.obj X)
-- Aesop.Options.Public
/-- Enable the builtin `simp` normalisation rule.
 -/
Aesop.Options.enableSimp : Aesop.Options → Bool
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.coe_ofLinearMap : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂)
  (g : M₂ →ₛₗ[σ₂₁] M) (h₁ : f ∘ₛₗ g = LinearMap.id) (h₂ : g ∘ₛₗ f = LinearMap.id),
  ⇑(LinearEquiv.ofLinearMap f g h₁ h₂) = ⇑f
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.Break.runK.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Init.Data.Range.Polymorphic.Char
_private.Init.Data.Range.Polymorphic.Char.0.Char.instPreservesLeast?FinNumCodePointsMap : Char.map✝.PreservesLeast?
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- When the category is `G`-Set, `cechNerveTerminalFrom` of `G` with the left regular action is
isomorphic to `EG`, the universal cover of the classifying space of `G` as a simplicial `G`-set.  -/
classifyingSpaceUniversalCover.cechNerveTerminalFromIso : (G : Type u) →
  [inst : Monoid G] → CategoryTheory.cechNerveTerminalFrom (Action.ofMulAction G G) ≅ classifyingSpaceUniversalCover G
-- Mathlib.GroupTheory.Transfer
AddMonoidHom.transfer.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {A : Type u_2} [inst_1 : AddCommGroup A] (ϕ : ↥H →+ A)
  [inst_2 : H.FiniteIndex],
  ϕ.transfer =
    { toFun := fun g => AddSubgroup.leftTransversals.diff ϕ default (g +ᵥ default), map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
/-- Note that `StarModule` is quite a strong requirement; as such we also provide the following
variants which this lemma would not apply to:
* `Matrix.conjTranspose_smul_non_comm`
* `Matrix.conjTranspose_nsmul`
* `Matrix.conjTranspose_zsmul`
* `Matrix.conjTranspose_natCast_smul`
* `Matrix.conjTranspose_intCast_smul`
* `Matrix.conjTranspose_inv_natCast_smul`
* `Matrix.conjTranspose_inv_intCast_smul`
* `Matrix.conjTranspose_ratCast_smul`
 -/
Matrix.conjTranspose_smul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : Star R] [inst_1 : Star α] [inst_2 : SMul R α]
  [StarModule R α] (c : R) (M : Matrix m n α), (c • M).conjTranspose = star c • M.conjTranspose
-- Mathlib.Data.Stream.Init
Stream'.get_succ : ∀ {α : Type u} (n : ℕ) (s : Stream' α), s.get n.succ = s.tail.get n
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.finrank_corootSpan_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  (S : Type u_5) [inst_6 : CommRing S] [IsDomain R] [IsDomain S] [inst_9 : Algebra S R] [FaithfulSMul S R]
  [P.IsValuedIn S] [inst_12 : Module S M] [IsScalarTower S R M] [inst_14 : Module S N] [IsScalarTower S R N]
  [P.IsAnisotropic], Module.finrank S ↥(P.corootSpan S) = Module.finrank S ↥(P.rootSpan S)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.insertMany_list_equiv_foldl : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] {l : List α},
  m.WF → (m.insertMany l).Equiv (List.foldl (fun acc a => acc.insert a) m l)
-- Mathlib.Order.Category.PartOrdEmb
/-- Given a predicate `P : Set α → Prop` on the underlying type of `α : PartOrdEmb.{u}`,
this is the functor `Subtype P ⥤ PartOrdEmb.{u}` which sends a subset `J` of `α`
satisfying `P` to the induced partially ordered type `J`.  -/
PartOrdEmb.functorOfPredicateSet : {α : PartOrdEmb} → (P : Set ↑α → Prop) → CategoryTheory.Functor (Subtype P) PartOrdEmb
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The inner product of two non-zero vectors equals the product of their norms
if and only if the angle between the two vectors is 0.  -/
InnerProductGeometry.inner_eq_mul_norm_iff_angle_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  x ≠ 0 → y ≠ 0 → (inner ℝ x y = ‖x‖ * ‖y‖ ↔ InnerProductGeometry.angle x y = 0)
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Submodule.det_reflection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : FiniteDimensional 𝕜 ↥K],
  LinearMap.det ↑K.reflection.toLinearEquiv = (-1) ^ Module.finrank 𝕜 ↥Kᗮ
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.getMaxHeartbeats : Lean.Options → ℕ
-- Lean.Parser.Do
Lean.Parser.Term.doIdDecl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Parser.Term
Lean.Parser.Term.idbg.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_le_iff : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderTop α] {s : Finset ι} {f : ι → α} {a : α},
  a < ⊤ → (s.inf f ≤ a ↔ ∃ b ∈ s, f b ≤ a)
-- Mathlib.Algebra.Group.Int.Even
Int.not_even_one : ¬Even 1
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_id : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₁.X₁ = X
-- Mathlib.Dynamics.Flow
Flow.mem_orbit : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) (x : α) (t : τ), ϕ.toFun t x ∈ ϕ.orbit x
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.unit_eq_unit : ∀ {C : Type u},
  CategoryTheory.FreeMonoidalCategory.unit =
    CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.FreeMonoidalCategory C)
-- Mathlib.Order.WellFoundedSet
/-- In the context of partial well-orderings, a bad sequence is a nonincreasing sequence
whose range is contained in a particular set `s`. One exists if and only if `s` is not
partially well-ordered.  -/
Set.PartiallyWellOrderedOn.IsBadSeq : {α : Type u_2} → (α → α → Prop) → Set α → (ℕ → α) → Prop
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.Valid.prevn : ∀ {it : String.Legacy.Iterator}, it.Valid → ∀ (n : ℕ), (it.prevn n).Valid
-- Init.Data.String.Basic
ByteArray.IsValidUTF8.push : ∀ {b : ByteArray}, b.IsValidUTF8 → ∀ {c : Char}, c.utf8Size = 1 → (b.push c.toUInt8).IsValidUTF8
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiff_congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {n : WithTop ℕ∞},
  (∀ (y : M), f₁ y = f y) → (ContMDiff I I' n f₁ ↔ ContMDiff I I' n f)
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.res_injective : ∀ {α : Type u_2}, Function.Injective PiNat.res
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.coeFn_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : ENNReal) (μ : MeasureTheory.Measure α) (G : Type u_7)
  [inst_1 : NormedAddCommGroup G], ↑↑↑0 =ᵐ[μ] 0
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.cuspFunction_neg : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  ContinuousAt (UpperHalfPlane.cuspFunction h f) 0 →
    UpperHalfPlane.cuspFunction h (-f) = -UpperHalfPlane.cuspFunction h f
-- Mathlib.Order.Disjointed
preimage_find_eq_disjointed : ∀ {α : Type u_1} (s : ℕ → Set α) (H : ∀ (x : α), ∃ n, x ∈ s n) [inst : (x : α) → (n : ℕ) → Decidable (x ∈ s n)] (n : ℕ),
  (fun x => Nat.find ⋯) ⁻¹' {n} = disjointed s n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false → (t.insertMany l).getD k fallback = t.getD k fallback
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.inclusion_injective : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L M : BooleanSubalgebra α} (h : L ≤ M),
  Function.Injective ⇑(BooleanSubalgebra.inclusion h)
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The weighted homogeneous components of an `MvPowerSeries f`.  -/
MvPowerSeries.weightedHomogeneousComponent : {σ : Type u_1} → {R : Type u_2} → [inst : Semiring R] → (σ → ℕ) → ℕ → MvPowerSeries σ R →ₗ[R] MvPowerSeries σ R
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instVAdd.eq_1 : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α], Colex.instVAdd = inst
-- Mathlib.Data.Fintype.BigOperators
Fintype.card_sigma : ∀ {ι : Type u_8} {α : ι → Type u_7} [inst : Fintype ι] [inst_1 : (i : ι) → Fintype (α i)],
  Fintype.card (Sigma α) = ∑ i, Fintype.card (α i)
-- Mathlib.Geometry.Manifold.Algebra.Structures
ContMDiffRing.contMDiff_mul : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
  {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {R : Type u_4} {inst_4 : Semiring R} {inst_5 : TopologicalSpace R} {inst_6 : ChartedSpace H R}
  [self : ContMDiffRing I n R], ContMDiff (I.prod I) I n fun p => p.1 * p.2
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerRight : Inhabited Mathlib.Tactic.BicategoryLike.WhiskerRight
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldl_eq_foldl_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {f : δ → α → β → δ}
  {init : δ}, Std.TreeMap.foldl f init t = Array.foldl (fun a b => f a b.1 b.2) init t.toArray
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- In the case of the manifold structure on a vector space, the extended charts are just the
identity.  -/
extChartAt_model_space_eq_id : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (x : E), extChartAt (modelWithCornersSelf 𝕜 E) x = PartialEquiv.refl E
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_simpleFunc_larger_space : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [CompleteSpace F] {β : Type u_6}
  {m m0 : MeasurableSpace β} {μ : MeasureTheory.Measure β},
  m ≤ m0 →
    ∀ (f : MeasureTheory.SimpleFunc β F),
      MeasureTheory.Integrable (⇑f) μ → ∫ (x : β), f x ∂μ = ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • x
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balance1.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c) z d)
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.red b y c)) z d)
  (h_3 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive a x b),
  (∀ (a_1 : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α), a = RBTree.RBNode.node RBTree.RBColor.red a_1 x b → False) →
    (match RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.red b y c), z, d with
      | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c, z, d =>
        h_1 a x b y c z d
      | RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.red b y c), z, d =>
        h_2 a x b y c z d
      | a, x, b => h_3 a x b) =
      h_2 a x b y c z d
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_whiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : Cᴹᵒᵖ}
  (f : X ⟶ Y) (Z : Cᴹᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z).unmop =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z.unmop f.unmop
-- Lean.Elab.PreDefinition.WF.GuessLex
_private.Lean.Elab.PreDefinition.WF.GuessLex.0.Lean.Elab.WF.GuessLex.withRecApps.loop : {α : Type} →
  (recFnName : Lean.Name) →
    ℕ → (Lean.Expr → Array Lean.Expr → Lean.MetaM α) → Lean.Expr → Lean.Expr → Lean.Elab.WF.GuessLex.M recFnName α Unit
-- Mathlib.CategoryTheory.Filtered.FinallySmall
CategoryTheory.InitiallySmall.instInitialCofilteredInitialModelFromCofilteredInitialModel : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofiltered C]
  [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] [inst_3 : CategoryTheory.InitiallySmall C],
  (CategoryTheory.InitiallySmall.fromCofilteredInitialModel C).Initial
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Given a sieve `S` on `X : C`, its associated diagram `S.diagram` is defined to be
the natural functor from the full subcategory of the over category `C/X` consisting
of arrows in `S` to `C`.  -/
CategoryTheory.Presieve.diagram : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → (S : CategoryTheory.Presieve X) → CategoryTheory.Functor S.category C
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The `v`-adic absolute value of a natural number is `≤ 1`.  -/
NumberField.HeightOneSpectrum.adicAbv_natCast_le_one : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (n : ℕ), (NumberField.HeightOneSpectrum.adicAbv K v) ↑n ≤ 1
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.coe_normUnit : ∀ {R : Type u} [inst : CommRing R] [inst_1 : NoZeroDivisors R] [inst_2 : NormalizationMonoid R] {p : Polynomial R},
  ↑(normUnit p) = Polynomial.C ↑(normUnit p.leadingCoeff)
-- Mathlib.Data.Nat.Choose.Multinomial
Finset.sum_pow_eq_sum_piAntidiag : ∀ {α : Type u_1} {R : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring R] (s : Finset α) (f : α → R) (n : ℕ),
  (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(Nat.multinomial s k) * ∏ i ∈ s, f i ^ k i
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} → (base : C) → ↑(F.obj base) → CategoryTheory.Grothendieck F
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalComp_cons : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g h i j : C} (α : f ≅ g) (η : g ⟶ h) {ηs : h ⟶ i}
  {θ : i ⟶ j} {ι : h ⟶ j},
  CategoryTheory.CategoryStruct.comp ηs θ = ι →
    CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) θ =
      CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ι)
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingAfter_def : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Preorder ι] [inst_1 : InfSet ι] (u : ι → Ω → β) (s : Set β)
  (n : ι),
  MeasureTheory.hittingAfter u s n = fun x => if ∃ j, n ≤ j ∧ u j x ∈ s then ↑(sInf {i | n ≤ i ∧ u i x ∈ s}) else ⊤
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopy.transAssocReparamAux_mem_I : ∀ (t : ↑unitInterval), Path.Homotopy.transAssocReparamAux t ∈ unitInterval
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {f : β k → β k}, k' ∈ t.modify k f ↔ k' ∈ t
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.continuous_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Continuous f ↔ ∀ (b : α), ∀ ε > 0, ∃ δ > 0, ∀ (a : α), dist a b < δ → dist (f a) (f b) < ε
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.Closed.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X : C} →
        (rightAdj : CategoryTheory.Functor C C) →
          (CategoryTheory.MonoidalCategory.tensorLeft X ⊣ rightAdj) → CategoryTheory.Closed X
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
/-- The additive action on an affine subspace corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.  -/
AffineSubspace.pointwiseAddAction : {k : Type u_2} →
  {V : Type u_3} →
    {P : Type u_4} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → AddAction V (AffineSubspace k P)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_le_max_of_aleph0_le_right : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ b → a * b ≤ max a b
-- Init.Data.List.Basic
List.intersperse_single : ∀ {α : Type u} {x sep : α}, List.intersperse sep [x] = [x]