mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxKey?.induct_unfolding : ∀ {α : Type u} {β : α → Type v} (motive : Std.DTreeMap.Internal.Impl α β → Option α → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf none →
    (∀ (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) (some k)) →
      (∀ (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
          (l_1 r : Std.DTreeMap.Internal.Impl α β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)
              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxKey? →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxKey?) →
        ∀ (a : Std.DTreeMap.Internal.Impl α β), motive a a.maxKey?
-- Mathlib.NumberTheory.ZetaValues
fourierCoeff_bernoulli_eq : ∀ {k : ℕ},
  k ≠ 0 →
    ∀ (n : ℤ),
      fourierCoeff (Complex.ofReal ∘ periodizedBernoulli k) n = -↑k.factorial / (2 * ↑Real.pi * Complex.I * ↑n) ^ k
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_sup_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F},
  Function.Surjective ⇑f → ∀ (S T : Submonoid N), Submonoid.map f (Submonoid.comap f S ⊔ Submonoid.comap f T) = S ⊔ T
-- Init.Data.String.Lemmas.FindPos
String.Slice.posLT.congr_simp : ∀ (s : String.Slice) (offset offset_1 : String.Pos.Raw) (e_offset : offset = offset_1) (_h : 0 < offset),
  s.posLT offset _h = s.posLT offset_1 ⋯
-- Mathlib.Order.Category.Semilat
SemilatSupCatEquivSemilatInfCat_inverse : SemilatSupCatEquivSemilatInfCat.inverse = SemilatInfCat.dual
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_toInt32 : ∀ (x : Int16), x.toInt32.toNatClampNeg = x.toNatClampNeg
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
/-- Whisker a `V`-enriched natural transformation on the right.  -/
CategoryTheory.EnrichedCat.whiskerRight : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₁} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              {E : Type u₂} →
                [inst_4 : CategoryTheory.EnrichedCategory V E] →
                  {F G : CategoryTheory.EnrichedFunctor V C D} →
                    (F ⟶ G) →
                      (H : CategoryTheory.EnrichedFunctor V D E) →
                        CategoryTheory.EnrichedFunctor.comp V F H ⟶ CategoryTheory.EnrichedFunctor.comp V G H
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H1ToTensorOfIsTrivial.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial],
  groupHomology.H1ToTensorOfIsTrivial A = groupHomology.H1ToTensorOfIsTrivial A
-- Init.Data.Fin.Lemmas
Fin.cast_natAdd : ∀ (n : ℕ) {m : ℕ} (i : Fin m), Fin.cast ⋯ (Fin.natAdd n i) = i.addNat n
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_apply : ∀ {α : Type u_2} {β : Type u_3} {C : β → Type u_7} [inst : (b : β) → SemilatticeSup (C b)] {s : Finset α}
  (H : s.Nonempty) (f : α → (b : β) → C b) (b : β), s.sup' H f b = s.sup' H fun a => f a b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_map : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α] {f : (a : α) → β a → γ a} {k : α},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.map f m).getKey! k = m.getKey! k
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.cylinder_eq_cylinder_union : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] (I : Finset ι) (S : Set ((i : ↥I) → α ↑i)) (J : Finset ι),
  MeasureTheory.cylinder I S = MeasureTheory.cylinder (I ∪ J) (Finset.restrict₂ ⋯ ⁻¹' S)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
/-- If two roots make an obtuse angle then their sum is a root (provided it is not zero).

See `RootPairing.pairingIn_le_zero_of_root_add_mem` for a partial converse.  -/
RootPairing.root_add_root_mem_of_pairingIn_neg : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [Finite ι]
  [CharZero R] [inst_7 : P.IsCrystallographic] {i j : ι} [IsDomain R],
  P.pairingIn ℤ i j < 0 → P.root i ≠ -P.root j → P.root i + P.root j ∈ Set.range ⇑P.root
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.binaryCofan_inr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B : C} [CategoryTheory.Limits.MonoCoprod C]
  (c : CategoryTheory.Limits.BinaryCofan A B) (hc : CategoryTheory.Limits.IsColimit c), CategoryTheory.Mono c.inr
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.coe_mk : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  (S : StarSubalgebra ℂ (H →L[ℂ] H)) (h : S.carrier.centralizer.centralizer = S.carrier),
  ↑{ toStarSubalgebra := S, centralizer_centralizer' := h } = ↑S
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.hom_right_inv_right_assoc : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (e : f ≅ g) {Z : T}
  (h : f.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right e.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right e.inv) h) =
    h
-- Mathlib.RingTheory.Spectrum.Prime.Defs
PrimeSpectrum.instPartialOrder : {R : Type u_1} → [inst : CommSemiring R] → PartialOrder (PrimeSpectrum R)
-- Lean.Elab.Level
Lean.Elab.Level.State.mk.injEq : ∀ (ngen : Lean.NameGenerator) (mctx : Lean.MetavarContext) (levelNames : List Lean.Name) (ngen_1 : Lean.NameGenerator)
  (mctx_1 : Lean.MetavarContext) (levelNames_1 : List Lean.Name),
  ({ ngen := ngen, mctx := mctx, levelNames := levelNames } =
      { ngen := ngen_1, mctx := mctx_1, levelNames := levelNames_1 }) =
    (ngen = ngen_1 ∧ mctx = mctx_1 ∧ levelNames = levelNames_1)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.Hom.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C}
  {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} {x y : A₀.Hom A₁}, x.f = y.f → x = y
-- Mathlib.GroupTheory.Complement
/-- The collection of left transversals of a subgroup  -/
Subgroup.LeftTransversal : {G : Type u_1} → [inst : Group G] → Subgroup G → Type (max 0 u_1)
-- Init.Data.UInt.Bitwise
UInt8.neg_one_xor : ∀ {a : UInt8}, -1 ^^^ a = ~~~a
-- Init.Guard
/-- Alpha-eq matching for `guard_hyp` types  -/
Lean.Parser.colonA : Lean.ParserDescr
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropyInf_closure : ∀ {X : Type u_1} {T : X → X} {F : Set X} [inst : UniformSpace X],
  Continuous T → Dynamics.coverEntropyInf T (closure F) = Dynamics.coverEntropyInf T F
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- The `BoxIntegral.IntegrationParams` corresponding to the Henstock-Kurzweil integral. In the
corresponding filter, we require that the tagged partition is subordinate to a (possibly,
discontinuous) positive function `r` and each tag belongs to the corresponding closed box.  -/
BoxIntegral.IntegrationParams.Henstock : BoxIntegral.IntegrationParams
-- Mathlib.RingTheory.Localization.FractionRing
/-- Given rings `A, B` and localization maps to their fraction rings
`f : A →+* K, g : B →+* L`, an isomorphism `h : A ≃+* B` induces an isomorphism of
fraction rings `K ≃+* L`.  -/
IsFractionRing.ringEquivOfRingEquiv : {A : Type u_8} →
  {K : Type u_9} →
    {B : Type u_10} →
      {L : Type u_11} →
        [inst : CommRing A] →
          [inst_1 : CommRing B] →
            [inst_2 : CommRing K] →
              [inst_3 : CommRing L] →
                [inst_4 : Algebra A K] →
                  [IsFractionRing A K] → [inst_6 : Algebra B L] → [IsFractionRing B L] → A ≃+* B → K ≃+* L
-- Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
Lean.Meta.Grind.Arith.CommRing.MonadRing.getRing : {m : Type → Type} → [self : Lean.Meta.Grind.Arith.CommRing.MonadRing m] → m Lean.Meta.Grind.Arith.CommRing.Ring
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAdd.contMDiff_add : ∀ {𝕜 : 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 ℕ∞}
  {G : Type u_4} {inst_4 : Add G} {inst_5 : TopologicalSpace G} {inst_6 : ChartedSpace H G} [self : ContMDiffAdd I n G],
  ContMDiff (I.prod I) I n fun p => p.1 + p.2
-- Mathlib.Algebra.Notation.Pi.Basic
/-- A congruence lemma for `Pi.mulSingle`, specialized for the non-dependent case. Without this,
`simp` can't rewrite in the first and third argument (`i` and `j`) because of dependence.
See also https://github.com/leanprover/lean4/issues/12478.
 -/
Pi.mulSingle_congr : ∀ {ι : Type u_1} [inst : DecidableEq ι] {M : Type u_9} [inst_1 : One M] {i₁ i₂ : ι},
  i₁ = i₂ → ∀ {x₁ x₂ : M}, x₁ = x₂ → ∀ {j₁ j₂ : ι}, j₁ = j₂ → Pi.mulSingle i₁ x₁ j₁ = Pi.mulSingle i₂ x₂ j₂
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Implementation of `AddMon.equivLaxMonoidalFunctorPUnit`.  -/
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addUnitIso : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor.id (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) ≅
        (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon C).comp
          (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal C)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.rightKanExtensionUnique_inv : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] (F'' : CategoryTheory.Functor D H) (α' : L.comp F'' ⟶ F)
  [inst_4 : F''.IsRightKanExtension α'],
  (F'.rightKanExtensionUnique α F'' α').inv = F'.liftOfIsRightKanExtension α F'' α'
-- Init.Sym.Lemmas
Lean.Sym.Int64.lt_eq_false : ∀ (a b : Int64), decide (a < b) = false → (a < b) = False
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.IsMultiplicative.prod_primeFactors : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {f : ArithmeticFunction R},
  f.IsMultiplicative → ∀ {l : ℕ}, Squarefree l → ∏ a ∈ l.primeFactors, f a = f l
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.bddAbove_l_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {s : Set α}, BddAbove (l '' s) ↔ BddAbove s
-- Mathlib.Analysis.Calculus.TangentCone.Real
uniqueDiffWithinAt_Ici : ∀ (x : ℝ), UniqueDiffWithinAt ℝ (Set.Ici x) x
-- Mathlib.Data.Num.Basic
/-- Addition of two `Num`s.  -/
Num.add : Num → Num → Num
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.skipSuffix?_eq_skipSuffix?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p],
  String.Slice.Pattern.BackwardPattern.skipSuffix? p =
    String.Slice.Pattern.BackwardPattern.skipSuffix? fun x => decide (p x)
-- Init.Data.UInt.Lemmas
USize.toUInt64_lt : ∀ {a b : USize}, a.toUInt64 < b.toUInt64 ↔ a < b
-- Mathlib.Topology.Order.IsLUB
Dense.exists_seq_strictMono_tendsto : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMinOrder α] [FirstCountableTopology α] {s : Set α},
  Dense s → ∀ (x : α), ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Set.Iio x ∩ s) ∧ Filter.Tendsto u Filter.atTop (nhds x)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.denote.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.Linarith.Poly → Sort u_1) (p : Lean.Grind.Linarith.Poly)
  (h_1 : Unit → motive Lean.Grind.Linarith.Poly.nil)
  (h_2 :
    (k : ℤ) →
      (v : Lean.Grind.Linarith.Var) → (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add k v p))
  (k : ℤ) (v : Lean.Grind.Linarith.Var) (p_1 : Lean.Grind.Linarith.Poly),
  p = Lean.Grind.Linarith.Poly.add k v p_1 →
    (match p with
      | Lean.Grind.Linarith.Poly.nil => h_1 ()
      | Lean.Grind.Linarith.Poly.add k v p => h_2 k v p) ≍
      h_2 k v p_1
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biproduct.matrix_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J K : Type}
  [inst_2 : Finite J] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] [inst_4 : Fintype K] {f : J → C}
  {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) {P : C} (x : (k : K) → g k ⟶ P) {Z : C} (h : P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc x) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.desc fun j => ∑ k, CategoryTheory.CategoryStruct.comp (m j k) (x k)) h
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.absolutelyContinuous_of_posterior : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧],
  (∀ᵐ (b : 𝓧) ∂μ.bind ⇑κ, ((ProbabilityTheory.posterior κ μ) b).AbsolutelyContinuous μ) →
    ∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getEntry?.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a k : α) (v : β k) (l : List ((a : α) × β a)),
  Std.Internal.List.getEntry? a (⟨k, v⟩ :: l) = bif k == a then some ⟨k, v⟩ else Std.Internal.List.getEntry? a l
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.zipWithLeft'TR.go.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (motive : List α → List β → Array γ → Sort u_4) (as : List α)
  (acc : Array γ) (h_1 : (bs : List β) → (acc : Array γ) → motive [] bs acc)
  (h_2 : (as : List α) → (acc : Array γ) → motive as [] acc)
  (h_3 : (a : α) → (as : List α) → (b : β) → (bs : List β) → (acc : Array γ) → motive (a :: as) (b :: bs) acc),
  (as = [] → False) →
    (match as, [], acc with
      | [], bs, acc => h_1 bs acc
      | as, [], acc => h_2 as acc
      | a :: as, b :: bs, acc => h_3 a as b bs acc) =
      h_2 as acc
-- Mathlib.FieldTheory.Galois.Infinite
InfiniteGalois.fixedField_bot : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K],
  IntermediateField.fixedField ⊤ = ⊥
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.zoom_zoomed₂ : ∀ {α : Type u_1} {cut : α → Ordering} {t : RBTree.RBNode α} {path : RBTree.RBNode.Path α} {t' : RBTree.RBNode α}
  {path' : RBTree.RBNode.Path α},
  RBTree.RBNode.zoom cut t path = (t', path') → RBTree.RBNode.Path.Zoomed cut path → RBTree.RBNode.Path.Zoomed cut path'
-- Lean.DocString.Types
Lean.Doc.Part.brecOn_1.eq : ∀ {i : Type u} {b : Type v} {p : Type w} {motive_1 : Lean.Doc.Part i b p → Sort u_1}
  {motive_2 : Array (Lean.Doc.Part i b p) → Sort u_1} {motive_3 : List (Lean.Doc.Part i b p) → Sort u_1}
  (t : Array (Lean.Doc.Part i b p)) (F_1 : (t : Lean.Doc.Part i b p) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Doc.Part i b p)) → Lean.Doc.Part.below_1 t → motive_2 t)
  (F_3 : (t : List (Lean.Doc.Part i b p)) → Lean.Doc.Part.below_2 t → motive_3 t),
  Lean.Doc.Part.brecOn_1 t F_1 F_2 F_3 = F_2 t (Lean.Doc.Part.brecOn_1.go t F_1 F_2 F_3).2
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.shiftClosure_bot : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A], ⊥.shiftClosure A = ⊥
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.homogeneousCore'_le : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A] (𝒜 : ι → σ) (I : Ideal A),
  Ideal.homogeneousCore' 𝒜 I ≤ I
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.spanningCoe_coe : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph), G'.coe.spanningCoe = G'.spanningCoe
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_monadMap_refl_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 β} {post : α → Pred} {epost : EPred} [Pure m] (x : m α),
  Std.Internal.Do.wp (monadMap f x) post epost = Std.Internal.Do.wp (f x) post epost
-- Mathlib.Topology.UniformSpace.Defs
mem_uniformity_of_eq : ∀ {α : Type ua} [inst : UniformSpace α] {x y : α} {s : SetRel α α}, s ∈ uniformity α → x = y → (x, y) ∈ s
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_one_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (CategoryTheory.Mon D)) (X : C),
  CategoryTheory.MonObj.one.app X = CategoryTheory.MonObj.one
-- Init.Data.String.Basic
String.Slice.Pos.ofSlice_le : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {pos : (s.slice p₀ p₁ h).Pos}, String.Slice.Pos.ofSlice pos ≤ p₁
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.instIsRightAdjointRestrictScalars : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  (ModuleCat.restrictScalars f).IsRightAdjoint
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a measure in a normed space, function from `StrongDual ℝ E` to
`ℂ` with `charFunDual μ L = ∫ v, exp (L v * I) ∂μ`.  -/
MeasureTheory.charFunDual : {E : Type u_2} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] → {mE : MeasurableSpace E} → MeasureTheory.Measure E → StrongDual ℝ E → ℂ
-- Mathlib.Algebra.Divisibility.Hom
map_dvd : ∀ {M : Type u_1} {N : Type u_2} [inst : Semigroup M] [inst_1 : Semigroup N] {F : Type u_3} [inst_2 : FunLike F M N]
  [MulHomClass F M N] (f : F) {a b : M}, a ∣ b → f a ∣ f b
-- Mathlib.Topology.UniformSpace.Equicontinuity
uniformEquicontinuous_iInf_dom : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_6} {β' : Type u_9} [uα : UniformSpace α] {u : κ → UniformSpace β'}
  {F : ι → β' → α} {k : κ}, UniformEquicontinuous F → UniformEquicontinuous F
-- Mathlib.Data.Finset.Card
Finset.eq_iff_card_le_of_subset : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → (t.card ≤ s.card ↔ s = t)
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.IsLinear.linear : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} {inst : Semiring R} {inst_1 : TopologicalSpace F}
  {inst_2 : TopologicalSpace B} {inst_3 : TopologicalSpace (Bundle.TotalSpace F E)} {inst_4 : AddCommMonoid F}
  {inst_5 : Module R F} {inst_6 : (x : B) → AddCommMonoid (E x)} {inst_7 : (x : B) → Module R (E x)}
  {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [self : Bundle.Trivialization.IsLinear R e],
  ∀ b ∈ e.baseSet, IsLinearMap R fun x => (↑e ⟨b, x⟩).2
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpIndL1Fin_smul : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)]
  (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : ℝ) (x : G),
  MeasureTheory.condExpIndL1Fin hm hs hμs (c • x) = c • MeasureTheory.condExpIndL1Fin hm hs hμs x
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.prodMap_apply : ∀ {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [inst : TopologicalSpace α₁]
  [inst_1 : TopologicalSpace α₂] [inst_2 : TopologicalSpace β₁] [inst_3 : TopologicalSpace β₂] (f : C(α₁, α₂))
  (g : C(β₁, β₂)) (a : α₁ × β₁), (f.prodMap g) a = Prod.map (⇑f) (⇑g) a
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.rightUnitor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : C × CategoryTheory.Discrete PUnit.{w + 1}),
  (CategoryTheory.prod.rightUnitor C).obj X = X.1
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.MVarErrorKind.implicitArg.injEq : ∀ (lctx : Lean.LocalContext) (ctx : Lean.Expr) (lctx_1 : Lean.LocalContext) (ctx_1 : Lean.Expr),
  (Lean.Elab.Term.MVarErrorKind.implicitArg lctx ctx = Lean.Elab.Term.MVarErrorKind.implicitArg lctx_1 ctx_1) =
    (lctx = lctx_1 ∧ ctx = ctx_1)
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.ofComp_kerCompPreimage : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_3} {T : Type u_7} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι) (x : ↥Q.ker),
  (Q.ofComp P).toAlgHom ↑(Q.kerCompPreimage P x) = ↑x
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiffOn.prodMk_space : ∀ {𝕜 : 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'] {F' : Type u_11} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F'] {s : Set M}
  {n : WithTop ℕ∞} {f : M → E'} {g : M → F'},
  ContMDiffOn I (modelWithCornersSelf 𝕜 E') n f s →
    ContMDiffOn I (modelWithCornersSelf 𝕜 F') n g s →
      ContMDiffOn I (modelWithCornersSelf 𝕜 (E' × F')) n (fun x => (f x, g x)) s
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Coloring.isIndepSet_colorClass : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) (c : α), G.IsIndepSet (C.colorClass c)
-- Mathlib.SetTheory.Ordinal.Rank
WellFoundedGT.rank_strictAnti : ∀ {α : Type u} [inst : Preorder α] [inst_1 : WellFoundedGT α], StrictAnti (IsWellFounded.rank fun x1 x2 => x1 > x2)
-- Mathlib.Data.Set.Card
Set.ncard_lt_ncard : ∀ {α : Type u_1} {s t : Set α}, s ⊂ t → autoParam t.Finite Set.ncard_lt_ncard._auto_1 → s.ncard < t.ncard
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.infEDist_empty : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α}, Metric.infEDist x ∅ = ⊤
-- Mathlib.Algebra.Category.Ring.Basic
/-- **Alias** of `CategoryTheory.ConcreteCategory.forget_map_eq_ofHom`. -/
RingCat.forget_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.forget C).map f = TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMonIdIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.mapAddMonIdIso =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.AddMon.mkIso (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).mapAddMon.obj X).X) ⋯ ⋯)
      ⋯